Sémantika programů

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

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

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).