Sémantika programů

Informace níže se nevztahují k současnému semestru.

Semestr: zimní 2021/22
Přednáška: Čtvrtek, 12:20, SU2 (liché týdny) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet

Aktuality

05.01.2022: Zadání třetí domácí úlohy je v lecture06.pdf. Termín pro odevzdání je 21. 1. 2022, stejně jako u druhé úlohy.
16.12.2021: Zadání druhé domácí úlohy je v lecture05.pdf. Termín pro odevzdání je 21. 1. 2022.
15.11.2021: Přednáška, která se měla konat 9.12.2021, se přesouvá na termín 16.12.2021. V původně plánovaném termínu 9.12.2021 proběhne přednáška z předmětu Úvod do middleware.
10.11.2021: Zadání první domácí úlohy je v lecture03.pdf. Termín pro odevzdání je 25. 11. 2021.

Přednášky

Datum	Název	Soubory
30. 9. 2021	Úvod, výroková logika, speciální teorie, kontrakty pro specifikaci programů	lecture01.pdf
14. 10. 2021	Indukce	lecture02.pdf, examples02.zip
11. 11. 2021	Pi a PiVC	lecture03.pdf, examples03.zip
25. 11. 2021	Částečná správnost	lecture04.pdf, examples04.zip
16. 12. 2021	Úplná správnost	lecture05.pdf, examples05.zip
6. 1. 2022	Strategie pro psaní anotací	lecture06.pdf, examples06.zip
6. 1. 2022	Reálné systémy pro verifikaci pomocí kontraktů	lecture07.pdf

Anotace

Cílem kurzu je seznámit studenty se základy sémantiky imperativních programovacích jazyků. Studenti budou seznámeni s nástrojem pro verifikaci vlastností programů. Zápočet bude udělen za vypracování tří domácích úloh malého rozsahu.

Sylabus

Představení pojmu sémantiky programů
Metody specifikace vlastností imperativních programů
Matematické základy specifikace
Dokazování vlastností programů

Literatura

A. R. Bradley, Z. Manna: The Calculus of Computation, Springer-Verlag, 2007
E. M. Clarke, O. Grumberg, D. A. Peled: Model Checking, MIT Press, 1999
J. Galenson: PiVC – Verifikující překladač jazyka Pi – https://github.com/jgalenson/piVC (upravený klient pro PiVC systém stáhněte zde).