Nazwa przykładowego przedmiotu: Różnice pomiędzy wersjami
| Linia 33: | Linia 33: | ||
* 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 | ||
| Linia 39: | Linia 40: | ||
* Logika Hoare'a, jej wykorzystanie i własności formalne | * Logika Hoare'a, jej wykorzystanie i własności formalne | ||
* Systematyczne konstruowanie poprawnych programów | * Systematyczne konstruowanie poprawnych programów | ||
== Zalecana literatura == | == Zalecana literatura == | ||
Wersja z 16:44, 8 cze 2006
(forma zajęć: wykład + ćwiczenia, wykład+laboratorium, wykład, laboratorium)
Krótki opis
treść opisu
Sylabus
Autor sylabusa
prof. dr hab. Andrzej Tarlecki tarlecki@mimuw.edu.pl
Nazwa zajęć:
Semantyka i weryfikacja programów
Typ zajęć:
wykład (30 godz.) + ćwiczenia (30 godz.)
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.
Wymagania wstępne:
Wstęp do programowania Wstęp do teorii mnogości i logiki
Sylabus:
- 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
Zalecana literatura
- Pozycja pierwsza
- Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, Wprowadzenie do algorytmów,WNT 2004.
Moduły
- Temat modułu pierwszego - wykład (Temat modułu pierwszego propozycja ćwiczeń)
- Temat modułu drugiego - wykład (Temat modułu drugiego propozycja ćwiczeń)
- Temat modułu 3 - wykład (Temat modułu 3 propozycja ćwiczeń)
- Temat modułu 4 - wykład (Temat modułu 4 propozycja ćwiczeń)
- Temat modułu 5 - wykład (Temat modułu 5 propozycja ćwiczeń)
- Temat modułu 6 - wykład (Temat modułu 6 propozycja ćwiczeń)
- Temat modułu 7 - wykład (Temat modułu 7 propozycja ćwiczeń)
- Temat modułu 8 - wykład (Temat modułu 8 propozycja ćwiczeń)
- Temat modułu 9 - wykład (Temat modułu 9 propozycja ćwiczeń)
- Temat modułu 10 - wykład (Temat modułu 10 propozycja ćwiczeń)
- Temat modułu 11 - wykład (Temat modułu 11 propozycja ćwiczeń)
- Temat modułu 12 - wykład (Temat modułu 12 propozycja ćwiczeń)
- Temat modułu 13 - wykład (Temat modułu 13 propozycja ćwiczeń)
- Temat modułu 14 - wykład (Temat modułu 14 propozycja ćwiczeń)
- Temat modułu piętnastego - wykład (Temat modułu piętnastego propozycja ćwiczeń)
Bibliografia
- Pozycja pierwsza
- Pozycja druga
Autorzy opracowania
- Autor pierwszy
- Autor drugi
