Semantyka i weryfikacja programów

1. Formalny opis języków programowania

2. Operacyjne i denotacyjne metody definiowania semantyki programów

3. Semantyczne definicje podstawowych konstrukcji programistycznych

4. Matematyczne podstawy semantyki denotacyjnej

5. Pojęcia poprawności programów: poprawność częściowa i całkowita

6. Metody dowodzenia poprawności programów

7. Logika Hoare'a, jej wykorzystanie i własności formalne

8. Podstawowe pojęcia algebry uniwersalnej i ich rola w opisie języków programowania

Wymagania wstępne:

- Wstęp do programowania (1000-211bWPI i/lub 1000-211bWPF)

- Podstawy matematyki (1000-211bPM)

- Języki, automaty i obliczenia (1000-214bJAO)

Wiedza. Student zna i rozumie:

- pojęcia składni i semantyki języków programowania, metody ich definiowania, a także definicje podstawowych konstrukcji programistycznych (K_W02, K_W03, K_W13);

- matematyczne podstawy i praktyczne techniki definiowania semantyki programów (K_W13);

- pojęcie poprawności programu względem formalnej specyfikacji (K_W02, K_W04, K_W13);

- metody formalne dowodzenia częściowej i całkowitej poprawności prostych programów (K_W04, K_W10, K_W13).

Umiejętności. Student potrafi:

- definiować semantykę prostych konstrukcji programistycznych, a także zrozumieć działanie konstrukcji programistycznych na podstawie ich opisów semantycznych (K_U01, K_U03);

- stosować metody formalnej weryfikacji do dowodzenia poprawmości prostych programów (K_U03, K_U07);

- uzasadnić poprawność programów odnosząc się do ich semantyki (K_U03).

Kompetencje. Student jest gotów:

- znać ograniczenia swojej wiedzy i rozumieć potrzebę dalszego kształcenia (K_K01);

- zrozumieć i docenić znaczenie precyzji i dokładności w formułowaniu problemów i uzasadnianiu poprawności rozwiązań (K_K03).