Semantyka i weryfikacja programów: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
| (Nie pokazano 52 wersji utworzonych przez 6 użytkowników) | |||
| Linia 1: | Linia 1: | ||
== 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 == | == Sylabus == | ||
=== | === Autorzy === | ||
Andrzej Tarlecki | * Marcin Engel | ||
* Sławomir Lasota | |||
* Andrzej Tarlecki | |||
=== Wymagania wstępne === | === Wymagania wstępne === | ||
| Linia 8: | Linia 16: | ||
=== Zawartość === | === Zawartość === | ||
* Formalny opis języków programowania | * Formalny opis języków programowania | ||
* Operacyjne i denotacyjne metody definiowania semantyki programów | * Operacyjne i denotacyjne metody definiowania semantyki programów | ||
| Linia 19: | Linia 26: | ||
* Systematyczne konstruowanie poprawnych programów | * Systematyczne konstruowanie poprawnych programów | ||
=== | === Literatura === | ||
# P. Dembiński, J. | # P. Dembiński, J. Manuszynski. ''Matematyczne metody definiowania języków programowania.'' WNT, 1981. | ||
# M. Gordon. Denotacyjny opis języków programowania. WNT, 1983. | # M. Gordon. ''Denotacyjny opis języków programowania.'' WNT, 1983. | ||
# D. Gries. The Science of Programming. Springer-Verlag, 1981. | # D. Gries. ''The Science of Programming.'' Springer-Verlag, 1981. | ||
# E. Dijkstra. Umiejętność programowania. WNT, 1978. | # E. Dijkstra. ''Umiejętność programowania.'' WNT, 1978. | ||
{{kotwica|moduły|}} | |||
== Moduły == | |||
=== Moduły wykładowe === | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 1|Wykład 1. Wprowadzenie]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 2|Wykład 2. Semantyka operacyjna]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 3| Wykład 3. Semantyka naturalna]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 4| Wykład 4. Semantyka denotacyjna. While programy]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 5| Wykład 5. Semantyka denotacyjna. Bloki i deklaracje]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 6| Wykład 6. Semantyka denotacyjna. Przekazywanie parametrów. Wejście/wyjście]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 7| Wykład 7. Semantyka denotacyjna. Kontynuacje]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 8| Wykład 8. Punkty stałe w porządkach zupełnych]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 9| Wykład 9. Elementy teorii dziedzin]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 10| Wykład 10. Logika Hoare'a. Poprawność częściowa]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 11| Wykład 11. Poprawność i relatywna pełność logiki Hoare'a]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 12| Wykład 12. Poprawność całkowita]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 13| Wykład 13. Wyprowadzanie poprawnych programów]] | |||
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 14| Wykład 14. Systematyczne konstruowanie modularnych programów]] | |||
<!--* [[Template:Semantyka_i_weryfikacja_programów/Wykład 15| Wykład 15. Modelowanie semantyki denotacyjnej w językach funkcyjnych]]--> | |||
=== Moduły ćwiczeniowe === | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 1|Ćwiczenia 1. Semantyka operacyjna 1]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 2|Ćwiczenia 2. Semantyka operacyjna 2]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 3|Ćwiczenia 3. Semantyka operacyjna 3/Semantyka naturalna 1]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 4|Ćwiczenia 4. Semantyka naturalna 2]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 5|Ćwiczenia 5. Semantyka naturalna 3]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 6|Ćwiczenia 6. Semantyka naturalna 4]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 7|Ćwiczenia 7. Semantyka denotacyjna 1]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 8|Ćwiczenia 8. Semantyka denotacyjna 2]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 9|Ćwiczenia 9. Semantyka denotacyjna 3]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 10|Ćwiczenia 10. Semantyka denotacyjna 4]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 11|Ćwiczenia 11. Semantyka denotacyjna 5]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 12|Ćwiczenia 12. Semantyka denotacyjna 6]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 13|Ćwiczenia 13. Weryfikacja programów 1]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 14|Ćwiczenia 14. Weryfikacja programów 2]] | |||
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 15|Ćwiczenia 15. Weryfikacja programów 3]] | |||
Aktualna wersja na dzień 14:58, 16 paź 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
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
- 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
Moduły wykładowe
- Wykład 1. Wprowadzenie
- Wykład 2. Semantyka operacyjna
- Wykład 3. Semantyka naturalna
- Wykład 4. Semantyka denotacyjna. While programy
- Wykład 5. Semantyka denotacyjna. Bloki i deklaracje
- Wykład 6. Semantyka denotacyjna. Przekazywanie parametrów. Wejście/wyjście
- Wykład 7. Semantyka denotacyjna. Kontynuacje
- Wykład 8. Punkty stałe w porządkach zupełnych
- Wykład 9. Elementy teorii dziedzin
- Wykład 10. Logika Hoare'a. Poprawność częściowa
- Wykład 11. Poprawność i relatywna pełność logiki Hoare'a
- Wykład 12. Poprawność całkowita
- Wykład 13. Wyprowadzanie poprawnych programów
- Wykład 14. Systematyczne konstruowanie modularnych programów
Moduły ćwiczeniowe
- Ćwiczenia 1. Semantyka operacyjna 1
- Ćwiczenia 2. Semantyka operacyjna 2
- Ćwiczenia 3. Semantyka operacyjna 3/Semantyka naturalna 1
- Ćwiczenia 4. Semantyka naturalna 2
- Ćwiczenia 5. Semantyka naturalna 3
- Ćwiczenia 6. Semantyka naturalna 4
- Ćwiczenia 7. Semantyka denotacyjna 1
- Ćwiczenia 8. Semantyka denotacyjna 2
- Ćwiczenia 9. Semantyka denotacyjna 3
- Ćwiczenia 10. Semantyka denotacyjna 4
- Ćwiczenia 11. Semantyka denotacyjna 5
- Ćwiczenia 12. Semantyka denotacyjna 6
- Ćwiczenia 13. Weryfikacja programów 1
- Ćwiczenia 14. Weryfikacja programów 2
- Ćwiczenia 15. Weryfikacja programów 3
