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

Autorzy

• Marcin Engel
• Slawomir Lasota
• 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

• Wykład 1. Wprowadzenie (Ćwiczenia 1. Semantyka operacyjna 1)
• Wykład 2. Semantyka operacyjna (Ćwiczenia 2. Semantyka operacyjna 2)
• Wykład 3. Semantyka naturalna (Ćwiczenia 3. Semantyka operacyjna 3/Semantyka naturalna 1)
• Wykład 4. Semantyka denotacyjna. While programy (Ćwiczenia 4. Semantyka naturalna 2)
• Wykład 5. Semantyka denotacyjna. Bloki i deklaracje (Ćwiczenia 5. Semantyka naturalna 3)
• Wykład 6. Semantyka denotacyjna. Przekazywanie parametrów. Wejście/wyjście (Ćwiczenia 6. Semantyka naturalna 4)
• Wykład 7. Semantyka denotacyjna. Kontynuacje (Ćwiczenia 7. Semantyka denotacyjna 1)
• Wykład 8. Punkty stałe w porządkach zupełnych (Ćwiczenia 8. Semantyka denotacyjna 2)
• Wykład 9. Elementy teorii dziedzin (Ćwiczenia 9. Semantyka denotacyjna 3)
• Wykład 10. Logika Hoare'a. Poprawność częściowa (Ćwiczenia 10. Semantyka denotacyjna 4)
• Wykład 11. Relatywna pełność logiki Hoare'a (Ćwiczenia 11. Semantyka denotacyjna 5)
• Wykład 12. Poprawność całkowita (Ćwiczenia 12. Semantyka denotacyjna 6)
• Wykład 13. Wyprowadzanie poprawnych programów (Ćwiczenia 13. Weryfikacja programów 1)
• Wykład 14. Systematyczne konstruowanie modularnych programów (Ćwiczenia 14. Weryfikacja programów 2)
• Wykład 15. Modelowanie semantyki denotacyjnej w językach funkcyjnych (Ćwiczenia 15. Weryfikacja programów 3)