Semantyka i weryfikacja programów

Sylabus

Autor

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.