Semestr: zimní 2020/21
Přednáška: Pátek, 10:40, Zoom (liché týdny – sudé kalendářní) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet
Přednáška: Pátek, 10:40, Zoom (liché týdny – sudé kalendářní) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet
Aktuality
- Zadání třetí domácí úlohy je v prednaska06.pdf. Termín pro odevzdání je 8. 1. 2021. Odkaz na kód k úloze je stejný jako k druhé úloze: selectsort.pi
- Zadání druhé domácí úlohy je v prednaska05.pdf. Termín pro odevzdání je 11. 12. 2020. Odkaz na kód k úloze: selectsort.pi
- Zadání první domácí úlohy je v prednaska03.pdf. Termín pro odevzdání je 13. 11. 2020.
Přednášky
| Datum | Název | Soubory |
|---|---|---|
| 2. 10. 2020 | Úvod, výroková logika, speciální teorie, kontrakty pro specifikace programů | prednaska01.pdf, záznam přednášky |
| 16. 10. 2020 | Indukce | prednaska02.pdf, záznam přednášky |
| 30. 10. 2020 | Pi a PiVC | prednaska03.pdf, záznam přednášky |
| 13. 11. 2020 | Částečná správnost | prednaska04.pdf, záznam přednášky, InsertionSort.pi, UnsortedUnion.pi |
| 27. 11. 2020 | Úplná správnost | prednaska05.pdf, záznam přednášky, Pytel-termination.pi, BubbleSort-termination.pi, QuickSort-termination.pi, MergeSort-termination.pi |
| 8. 12. 2020 | Strategie pro psaní anotací | prednaska06.pdf, záznam přednášky, QuickSort.pi |
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).