Semantyka i weryfikacja programów

== Autor sylabusa prof. dr hab. Andrzej Tarlecki

==Typ zajęć wykład (30 godz.) + ćwiczenia (30 godz.)

== Wymagania wstępne

• Wstęp do programowania
• Wstęp do teorii mnogości i logiki

== Zawartość

• Formalny opis języków programowania
• Operacyjne i denotacyjne metody definiowania semantyki programów

• Semantyczne definicje podstawowych konstrukcji programistycznych
• Matematyczne podstawy semantyki denotacyjnej
• Pojęcia poprawności programów: poprawność częściowa i całkowita
• Metody dowodzenia poprawności programów
• Logika Hoare'a, jej wykorzystanie i własności formalne
• Systematyczne konstruowanie poprawnych programów

Zalecana literatura

1. P. Dembiński, J. Mańuszynski. Matematyczne metody definiowania języków programowania. WNT, 1981.
2. M. Gordon. Denotacyjny opis języków programowania. WNT, 1983.
3. D. Gries. The Science of Programming. Springer-Verlag, 1981.
4. E. Dijkstra. Umiejętność programowania. WNT, 1978.