Semantyka i weryfikacja programów

Forma zajęć

Wykład (30 godzin) + ćwiczenia (30 godzin)

Opis

Celem wykładu jest pokazanie roli i najważniejszych problemów i technik formalizacji opisu programów. Omawiane będą metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami. Wprowadzone zostaną pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia. Przedstawione też będą najważniejsze idee systematycznego konstruowania poprawnych programów.

Sylabus

Autor

• Andrzej Tarlecki

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

Literatura

1. P. Dembiński, J. Manuszynski. 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.

Moduły

• Semantyka operacyjna 1 (Ćwiczenia 1)
• Semantyka operacyjna 2 (Ćwiczenia 2)
• Semantyka naturalna 1 (Ćwiczenia 3)
• Semantyka naturalna 2 (Ćwiczenia 4)
• Semantyka naturalna 3 (Ćwiczenia 5)
• Semantyka naturalna 4 (Ćwiczenia 6)