460-4145/01 – Interaktivní a automatizované dokazování korektnosti programů (IADKP)
Garantující katedra | Katedra informatiky | Kredity | 4 |
Garant předmětu | doc. Ing. Zdeněk Sawa, Ph.D. | Garant verze předmětu | doc. Ing. Zdeněk Sawa, Ph.D. |
Úroveň studia | pregraduální nebo graduální | Povinnost | volitelný odborný |
Ročník | 1 | Semestr | letní |
| | Jazyk výuky | čeština |
Rok zavedení | 2022/2023 | Rok zrušení | |
Určeno pro fakulty | FEI | Určeno pro typy studia | navazující magisterské |
Cíle předmětu vyjádřené dosaženými dovednostmi a kompetencemi
Studenti se v tomto předmětu seznámí s problematikou formálního dokazování korektnosti programů a s použitím nástrojů pro interaktivní a automatizované dokazování, které je možné pro tyto účely využít. Cílem je seznámit se s tím, jak může být sémantika programovacích jazyků formalizována a jak mohou být vlastnosti programů formalizovány a dokazovány pomocí prostředků jako je Hoarova logika, separační logika a teorie typů. Studenti se naučí, jak mohou být takové prostředky formalizovány a implementovány v softwarových nástrojích jako je např. systém Coq, které mohou být využity pro částečně automatizované vytváření důkazů a automatizovanou kontrolu korektnosti těchto důkazů.
Vyučovací metody
Přednášky
Cvičení (v učebně)
Anotace
Předmět v sobě kombinuje několik témat - interaktivní a automatizované dokazování, sémantiku programovacích jazyků a dokazování korektnosti programů. Cílem se seznámit studenty s tím, jakým způsobem je možné pomocí softwarových nástrojů pro interaktivní a automatizované dokazování vytvářet formální počítačem ověřené důkazy korektnosti programů.
Existuje celá řada softwarových nástrojů, které umožňují interaktivně vytvářet důkazy, přičemž automaticky kontrolují správnost těchto důkazů a do určité míry umožňují automatizovat některé mechanické kroky důkazu.
První část semestru bude věnována primárně základům práce s jedním z takových softwarových nástrojů, se systémem Coq, který pak bude v další části semestru využíván pro dokazování korektnosti programů.
V této druhé části semestru budou probírána témata související s různými metodami dokazování této korektnosti. Aby bylo vůbec možné nějaké takové formální důkazy vytvářet, nejprve musí být formálně reprezentována sémantika programů. Část přednášek tedy bude věnovaná této problematice a také teorii typů, což je téma, které s výše uvedeným úzce souvisí. Dále pak budou studovány logiky používané pro dokazování vlastností programů - Hoarova logika a separační logika (což je modernější a obecnější rozšíření Hoarovy logiky o možnost dokazování korektnosti programů, které pracují s ukazateli a dynamicky alokovanými datovými strukturami).
Povinná literatura:
[1] Benjamin C. Pierce et al. - Software Foundations (volumes 1 - 5). Electronic textbook, version 5.8., 2020. Dostupné na adrese https://softwarefoundations.cis.upenn.edu
Doporučená literatura:
[2] Yves Bertot, Pierre Castéran - Interactive Theorem Proving and Program Development, Springer, 2004.
[3] Andrew W. Appel et al. - Program Logics for Certified Compilers, Cambridge University Press, 2014.
[4] Adam Chlipala - Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013.
[5] Benjamin C. Pierce - Types and Programming Languages, MIT Press, 2002.
[6] Benjamin C. Pierce, ed. - Advanced Topics in Types and Programming Languages. MIT Press, 2004.
[7] Glynn Winskel - Formal Semantics of Programming Languages, The MIT Press, 1993.
[8] Hans Hüttel - Transitions and Trees: An Introduction to Structural Operational Semantics, Cambridge University Press, 2010.
Forma způsobu ověření studijních výsledků a další požadavky na studenta
V průběhu semestru studenti vypracovávají řešení zadaných úloh v programu Coq.
Na závěr semestru vypracují v programu Coq kompletní důkaz korektnosti nějakého zadaného algoritmu.
Předmět je zakončen zkouškou, která se skládá z písemné a ústní části.
E-learning
Další požadavky na studenta
Na studenty nejsou kladeny další požadavky.
Prerekvizity
Předmět nemá žádné prerekvizity.
Korekvizity
Předmět nemá žádné korekvizity.
Osnova předmětu
Přednášky:
1. Úvod. Funkcionální programování v systému Coq.
2. Důkazy indukcí. Práce s datovými strukturami.
3. Polymorfismus a funkce vyššího řádu.
4. Základy logiky v systému Coq. Používání taktik v důkazech.
5. Induktivně definovaná tvrzení. Dokazování vlastností relací.
6. Formalizace syntaxe a sémantiky jednoduchého imperativního jazyka.
7. Strukturální operační sémantika.
8. Ekvivalence programů.
9. Logiky pro dokazování vlastností programů: Hoarova logika a separační logika.
10. Typové systémy.
11. Dokazování vlastností typových systémů.
12. Dokazování vlastností funkcionálních programů.
13. Verifikace implementace datových struktur.
Cvičení:
1. Seznámení se se systémem Coq.
2. Základy funkcionálního programování v Coqu.
3. Jednoduché důkazy v systému Coq.
4. Základy logiky v systému Coq. Používání taktik v důkazech.
5. Další techniky důkazů v Coqu.
6. Formalizace syntaxe a sémantiky jednoduchého imperativního jazyka.
7. Formalizace sémantiky jednoduchého imperativního jazyka v Coqu.
8. Dokazování některých vlastností programů.
9. Formalizace Hoarovy logiky v Coqu, důkaz korektnosti konkrétního jednoduchého algoritmu.
10. Další důkazy korektnosti algoritmů pomocí Hoarovy logiky.
11. Formalizace jednoduchého typového systému v Coqu.
12. Dokazování vlastností funkcionálních programů.
13. Verifikace implementace datových struktur.
Podmínky absolvování předmětu
Výskyt ve studijních plánech
Výskyt ve speciálních blocích
Hodnocení Výuky
Předmět neobsahuje žádné hodnocení.