Semestr: zimní 2024/25
Přednáška: Úterý, 15:40, S11 (Jan Kofroň)
Stránka v SIS: NSWI183
Zakončení: Zápočet
Přednáška: Úterý, 15:40, S11 (Jan Kofroň)
Stránka v SIS: NSWI183
Zakončení: Zápočet
Aktuality
- Zadání třetí domácí úlohy je v materiálech z přednášky 6. Termín pro odevzdání řešení je 26.11.2024.
- Zadání druhé domácí úlohy je v materiálech z přednášky 5. Termín pro odevzdání řešení je 12.11.2024.
- Zadání první domácí úlohy je v materiálech z přednášky 3. Termín pro odevzdání řešení je 29.10.2024.
Přednášky
| Datum | Název | Soubory |
|---|---|---|
| 01. 10. 2024 | Úvod, výroková logika, speciální teorie, kontrakty pro specifikaci programů | Přednáška 1 |
| 08. 10. 2024 | Indukce | Přednáška 2, Příklady 2 |
| 15. 10. 2024 | Pi a PiVC | Přednáška 3, Příklady 3 |
| 22. 10. 2024 | Částečná správnost | Přednáška 4, Příklady 4 |
| 29. 10. 2024 | Úplná správnost | Přednáška 5, Příklady 5 |
| 12. 11. 2024 | Strategie pro psaní anotací | Přednáška 6, QuickSort |
| 26. 11. 2024 | Reálné systémy pro verifikaci pomocí kontraktů | Přednáška 7, Příklady 7 |
| 3. 12. 2024 | Dafny | Přednáška 8, Příklady 8 |
| 10. 12. 2024 | Dafny | Přednáška 9, Příklady 9 |
| 17. 12. 2024 | Dafny |
Anotace
Cílem kurzu je seznámit studenty se základy sémantiky imperativních programovacích jazyků. Studenti budou seznámeni s nástroji pro verifikaci vlastností programů – PiVC a Dafny. Zápočet bude udělen za vypracování tří domácích úloh menšího rozsahu a jedné složitější úlohy.
Sylabus
- Představení pojmu sémantiky programů
- Metody specifikace vlastností imperativních programů
- Matematické základy specifikace
- Dokazování vlastností programů
- Programovací jazyk Dafny
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).
- The Dafny Programming and Verification Language