Semestr: zimní 2025/26
Přednáška: Pondělí, 10:40, S7 (Jan Kofroň)
Stránka v SIS: NSWI183
Zakončení: Zápočet

Stránky z předchozího roku: 2024/25

Aktuality

Přednášky

Datum Název Soubory
29. 09. 2025 Úvod, výroková logika, speciální teorie, kontrakty pro specifikaci programů Přednáška 1
06. 10. 2025 Indukce Přednáška 2, Příklady 2
13. 10. 2025 Pi a PiVC Přednáška 3, Příklady 3
20. 10. 2025 Částečná správnost Přednáška 4, Příklady 4
27. 10. 2025 Úplná správnost Přednáška 5, Příklady 5
03. 11. 2025 Strategie pro psaní anotací Přednáška 6, QuickSort
10. 11. 2025 Reálné systémy pro verifikaci pomocí kontraktů Přednáška 7, Příklady 7
24. 11. 2025 Dafny Přednáška 8, Příklady 8
01. 12. 2025 Dafny Přednáška 9, Příklady 9
08. 12. 2025 Dafny Přednáška 10, Příklady 10
15. 12. 2025 Dafny Přednáška 11, Příklady 11
05. 01. 2026 Dafny Přednáška 12, Příklady 12
05. 01. 2026 Dafny Přednáška 13, Příklady 13

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

Literatura