Semantyka i weryfikacja programów: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
| Linia 39: | Linia 39: | ||
* [[Semantyka_i_weryfikacja_programów/Moduł 5| Semantyka naturalna 3]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 5|Ćwiczenia 5]]) | * [[Semantyka_i_weryfikacja_programów/Moduł 5| Semantyka naturalna 3]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 5|Ćwiczenia 5]]) | ||
* [[Semantyka_i_weryfikacja_programów/Moduł 6| Semantyka naturalna 4]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 6|Ćwiczenia 6]]) | * [[Semantyka_i_weryfikacja_programów/Moduł 6| Semantyka naturalna 4]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 6|Ćwiczenia 6]]) | ||
* [[Semantyka_i_weryfikacja_programów/Moduł 7| Semantyka denotacyjna 1]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 7|Ćwiczenia 7]]) | |||
* [[Semantyka_i_weryfikacja_programów/Moduł 8| Semantyka denotacyjna 2]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 8|Ćwiczenia 8]]) | |||
* [[Semantyka_i_weryfikacja_programów/Moduł 9| Semantyka denotacyjna 3]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 9|Ćwiczenia 9]]) | |||
* [[Semantyka_i_weryfikacja_programów/Moduł 10| Semantyka denotacyjna 4]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 10|Ćwiczenia 10]]) | |||
* [[Semantyka_i_weryfikacja_programów/Moduł 11| Semantyka denotacyjna 5]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 11|Ćwiczenia 11]]) | |||
* [[Semantyka_i_weryfikacja_programów/Moduł 12| Semantyka denotacyjna 6]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 12|Ćwiczenia 12]]) | |||
* [[Semantyka_i_weryfikacja_programów/Moduł 13| Weryfikacja 1]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 13|Ćwiczenia 13]]) | |||
* [[Semantyka_i_weryfikacja_programów/Moduł 14| Weryfikacja 2]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 14|Ćwiczenia 14]]) | |||
* [[Semantyka_i_weryfikacja_programów/Moduł 15| Weryfikacja 3]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 15|Ćwiczenia 15]]) | |||
Wersja z 09:18, 5 sie 2006
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
- P. Dembiński, J. Manuszynski. Matematyczne metody definiowania języków programowania. WNT, 1981.
- M. Gordon. Denotacyjny opis języków programowania. WNT, 1983.
- D. Gries. The Science of Programming. Springer-Verlag, 1981.
- 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)
- Semantyka denotacyjna 1 (Ćwiczenia 7)
- Semantyka denotacyjna 2 (Ćwiczenia 8)
- Semantyka denotacyjna 3 (Ćwiczenia 9)
- Semantyka denotacyjna 4 (Ćwiczenia 10)
- Semantyka denotacyjna 5 (Ćwiczenia 11)
- Semantyka denotacyjna 6 (Ćwiczenia 12)
- Weryfikacja 1 (Ćwiczenia 13)
- Weryfikacja 2 (Ćwiczenia 14)
- Weryfikacja 3 (Ćwiczenia 15)
