Semantyka i weryfikacja programów: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
|||
| 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 == | ||
=== Autor === | === Autor === | ||
Andrzej Tarlecki | * Andrzej Tarlecki | ||
=== Wymagania wstępne === | === Wymagania wstępne === | ||
| Linia 8: | Linia 14: | ||
=== 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 20: | Linia 25: | ||
=== Literatura === | === 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. | ||
== Moduły == | |||
Wersja z 08:27, 9 cze 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.
