MIMINF:Semantyka i weryfikacja programów: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
|||
| (Nie pokazano 1 pośredniej wersji utworzonej przez tego samego użytkownika) | |||
| Linia 3: | Linia 3: | ||
== Opis == | == Opis == | ||
Rola, najważniejsze problemy i techniki formalizacji opisu programów. Metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami. Pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia. Najważniejsze idee systematycznego konstruowania poprawnych programów. | |||
== Sylabus == | == Sylabus == | ||
| Linia 18: | Linia 18: | ||
* 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 | ||
* Semantyczne definicje podstawowych konstrukcji programistycznych | * Semantyczne definicje podstawowych konstrukcji programistycznych | ||
* Matematyczne podstawy semantyki denotacyjnej | * Matematyczne podstawy semantyki denotacyjnej | ||
Aktualna wersja na dzień 12:53, 11 sty 2007
Forma zajęć
Wykład (30 godzin) + ćwiczenia (30 godzin)
Opis
Rola, najważniejsze problemy i techniki formalizacji opisu programów. Metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami. Pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia. 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.
