Nazwa przykładowego przedmiotu

(forma zajęć: wykład + ćwiczenia, wykład+laboratorium, wykład, laboratorium)

Krótki opis

treść opisu

Sylabus

Autor sylabusa

prof. dr hab. Andrzej Tarlecki tarlecki@mimuw.edu.pl

Nazwa zajęć:

Semantyka i weryfikacja programów

Typ zajęć:

wykład (30 godz.) + ćwiczenia (30 godz.)

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.

Wymagania wstępne:

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

Sylabus:

• 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.

Moduły

• Temat modułu pierwszego - wykład (Temat modułu pierwszego propozycja ćwiczeń)
• Temat modułu drugiego - wykład (Temat modułu drugiego propozycja ćwiczeń)
• Temat modułu 3 - wykład (Temat modułu 3 propozycja ćwiczeń)
• Temat modułu 4 - wykład (Temat modułu 4 propozycja ćwiczeń)
• Temat modułu 5 - wykład (Temat modułu 5 propozycja ćwiczeń)
• Temat modułu 6 - wykład (Temat modułu 6 propozycja ćwiczeń)
• Temat modułu 7 - wykład (Temat modułu 7 propozycja ćwiczeń)
• Temat modułu 8 - wykład (Temat modułu 8 propozycja ćwiczeń)
• Temat modułu 9 - wykład (Temat modułu 9 propozycja ćwiczeń)
• Temat modułu 10 - wykład (Temat modułu 10 propozycja ćwiczeń)
• Temat modułu 11 - wykład (Temat modułu 11 propozycja ćwiczeń)
• Temat modułu 12 - wykład (Temat modułu 12 propozycja ćwiczeń)
• Temat modułu 13 - wykład (Temat modułu 13 propozycja ćwiczeń)
• Temat modułu 14 - wykład (Temat modułu 14 propozycja ćwiczeń)
• Temat modułu piętnastego - wykład (Temat modułu piętnastego propozycja ćwiczeń)

Bibliografia

1. Pozycja pierwsza
2. Pozycja druga

Autorzy opracowania

1. Autor pierwszy
2. Autor drugi