MIMINF:Semantyka i weryfikacja programów

Forma zajęć

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

Opis

Rola, najważniejsze problemy i techniki formalizacji opisu programów. Metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami. Pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia. Najważniejsze idee systematycznego konstruowania poprawnych programów.

Sylabus

Autorzy

• Marcin Engel
• Sławomir 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.