Semantyka i weryfikacja programów: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
| Linia 41: | Linia 41: | ||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 7| Wykład 7. Semantyka denotacyjna. Kontynuacje]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 7|Ćwiczenia 7. Semantyka denotacyjna 1]]) | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 7| Wykład 7. Semantyka denotacyjna. Kontynuacje]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 7|Ćwiczenia 7. Semantyka denotacyjna 1]]) | ||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 8| Wykład 8. Punkty stałe w porządkach zupełnych]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 8|Ćwiczenia 8. Semantyka denotacyjna 2]]) | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 8| Wykład 8. Punkty stałe w porządkach zupełnych]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 8|Ćwiczenia 8. Semantyka denotacyjna 2]]) | ||
* [[Semantyka_i_weryfikacja_programów/Wykład 9| Wykład 9. | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 9| Wykład 9. Elementy teorii dziedzin]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 9|Ćwiczenia 9. Semantyka denotacyjna 3]]) | ||
* [[Semantyka_i_weryfikacja_programów/Wykład 10 | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 10| Wykład 10. Logika Hoare'a. Poprawność częściowa]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 10|Ćwiczenia 10. Semantyka denotacyjna 4]]) | ||
* [[Semantyka_i_weryfikacja_programów/ | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 11| Wykład 11. Relatywna pełność logiki Hoare'a]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 11|Ćwiczenia 11. Semantyka denotacyjna 5]]) | ||
* [[Semantyka_i_weryfikacja_programów/ | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 12| Wykład 12. Poprawność całkowita]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 12|Ćwiczenia 12. Semantyka denotacyjna 6]]) | ||
* [[Semantyka_i_weryfikacja_programów/ | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 13| Wykład 13. Wyprowadzanie poprawnych programów]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 13|Ćwiczenia 13. Weryfikacja programów 2]]) | ||
* [[Semantyka_i_weryfikacja_programów/ | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 14| Wykład 14. Systematyczne konstruowanie modularnych programów]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 14|Ćwiczenia 14. Weryfikacja programów 2]]) | ||
* [[Semantyka_i_weryfikacja_programów/ | * [[Template:Semantyka_i_weryfikacja_programów/Wykład 15| Modelowanie semantyki denotacyjnej w językach funkcyjnych]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 15|Ćwiczenia 15. Weryfikacja programów 3]]) | ||
Wersja z 10:37, 10 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
- 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 2)
- Wykład 14. Systematyczne konstruowanie modularnych programów (Ćwiczenia 14. Weryfikacja programów 2)
- Modelowanie semantyki denotacyjnej w językach funkcyjnych (Ćwiczenia 15. Weryfikacja programów 3)
