Přednáška: Pátek, 10:40, SU1 (liché týdny -- sudé kalendářní) (Jan Kofroň)
Stránka v SIS: NSWI162
Zakončení: Zápočet

Aktuality

Přednášky

Datum Název Soubory
4. 10. 2019 Úvod, výroková logika, speciální teorie, kontrakty pro specifikace programů prednaska01.pdf
18. 10. 2019 Indukce prednaska02.pdfLinearSearch.pi
1. 11. 2019 Pi a PiVC prednaska03.pdf
15. 11. 2019 Částečná správnost prednaska04.pdfUnsortedUnion-soln.piInsertionSort-soln.pi
29. 11. 2019 Úplná správnost prednaska05.pdfPytel-termination.piBubbleSort-termination.piQuickSort-termination.piMergeSort-termination.pi
13. 12. 2019 Strategie pro psaní anotací prednaska06.pdfQuickSort.pi
10. 1. 2020 Reálné systémy pro verifikaci pomocí kontraktů prednaska07.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

Literatura