460-4145/01 – Interaktivní a automatizované dokazování korektnosti programů (IADKP)

Garantující katedraKatedra informatikyKredity4
Garant předmětudoc. Ing. Zdeněk Sawa, Ph.D.Garant verze předmětudoc. Ing. Zdeněk Sawa, Ph.D.
Úroveň studiapregraduální nebo graduálníPovinnostvolitelný odborný
Ročník1Semestrletní
Jazyk výukyčeština
Rok zavedení2022/2023Rok zrušení
Určeno pro fakultyFEIUrčeno pro typy studianavazující magisterské
Výuku zajišťuje
Os. čís.JménoCvičícíPřednášející
SAW75 doc. Ing. Zdeněk Sawa, Ph.D.
Rozsah výuky pro formy studia
Forma studiaZp.zak.Rozsah
prezenční Zápočet a zkouška 2+2
kombinovaná Zápočet a zkouška 10+0

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

Prezenční forma (platnost od: 2022/2023 zimní semestr)
Název úlohyTyp úlohyMax. počet bodů
(akt. za podúlohy)
Min. počet bodůMax. počet pokusů
Zápočet a zkouška Zápočet a zkouška 100 (100) 51
        Zápočet Zápočet 35 (35) 20
                Řešení zadaných problémů Jiný typ úlohy 15  7
                Důkaz koreknosti zadaného programu Projekt 20  10
        Zkouška Zkouška 65  30 3
Rozsah povinné účasti: Účast na cvičeních je povinná a je kontrolována. S rozsahem povinné účastí seznámí studenty garant předmětu na začátku semestru.

Zobrazit historii

Podmínky absolvování předmětu a účast na cvičeních v rámci ISP: Splnění všech povinných úkolů v individuálně dohodnutých termínech. Rozsah účasti na cvičeních si student na začátku semestru dohodne s garantem předmětu.

Zobrazit historii

Výskyt ve studijních plánech

Akademický rokProgramObor/spec.Spec.ZaměřeníFormaJazyk výuky Konz. stř.RočníkZLTyp povinnosti
2024/2025 (N0613A140034) Informatika P čeština Ostrava 1 volitelný odborný stu. plán
2024/2025 (N0613A140034) Informatika K čeština Ostrava 1 volitelný odborný stu. plán
2023/2024 (N0613A140034) Informatika K čeština Ostrava 1 volitelný odborný stu. plán
2023/2024 (N0613A140034) Informatika P čeština Ostrava 1 volitelný odborný stu. plán
2022/2023 (N0613A140034) Informatika P čeština Ostrava 1 volitelný odborný stu. plán
2022/2023 (N0613A140034) Informatika K čeština Ostrava 1 volitelný odborný stu. plán

Výskyt ve speciálních blocích

Název blokuAkademický rokForma studiaJazyk výuky RočníkZLTyp blokuVlastník bloku

Hodnocení Výuky

Předmět neobsahuje žádné hodnocení.