Garant, přednášející, cvičící i tutor pro studenty v kombinované formě studia:
- doc. Ing. Zdeněk Sawa, Ph.D. (místnost: EA413, e-mail: zdenek.sawa@vsb.cz)
Zde se budou v průběhu semestru objevovat aktuální informace týkající se předmětu IADKP.
Předmět v sobě kombinuje několik témat:
- interaktivní a automatizované dokazování
- sémantiku programovacích jazyků
- dokazování korektnosti programů
Cílem je 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 tutoriálů 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).
Předběžný program přednášek:
- Úvod. Funkcionálnı́ programovánı́ v systému Coq.
- Důkazy indukcı́. Práce s datovými strukturami.
- Polymorfismus a funkce vyššı́ho řádu.
- Základy logiky v systému Coq. Použı́vánı́ taktik v důkazech.
- Induktivně definovaná tvrzenı́. Dokazovánı́ vlastnostı́ relacı́.
- Formalizace syntaxe a sémantiky jednoduchého imperativnı́ho jazyka.
- Strukturálnı́ operačnı́ sémantika. Ekvivalence programů.
- Logika pro dokazovánı́ vlastnostı́ programů — Hoarova logika.
- Separačnı́ logika.
- Typové systémy. Dokazovánı́ vlastnostı́ typových systémů.
- Dokazovánı́ vlastnostı́ funkcionálnı́ch programů.
Předběžný program tutoriálů:
- 1. tutoriál:
Na tomto úvodním tutoriálu budou studentům sděleny informace o organizaci studia předmětu a informace o náplni předmětu. Budou probírány základy práce se systémem Coq. Studenti se seznámí s funkcionálním programováním v systému Coq a prvními jednoduchými důkazy v tomto systému.
- 2. tutoriál:
Na tomto tutoriálu budou nejprve probírány některé další prvky funkcionálního jazyka Coqu, jako polymorfismus a funkce vyššího řádu. Hlavním tématem pak budou základy logiky v systému Coq, vytváření důkazů v Coqu a používání taktik v důkazech. Speciálně budou též diskutovány induktivní definice a důkazy indukcí.
- 3. tutoriál:
Na tomto tutoriálu bude probíráno, jakým způsobem je možné v systému Coq formálně reprezentovat syntaxi a sémantiku jednoduchého imperativního jazyka. V této souvislosti bude probíráno, jakým způsobem je možné obecně popisovat sémantiku programovacích jazyků pomocí strukturální operační sémantiky. Stručně bude též diskutována problematika dokazování ekvivalence programů.
- 4. tutoriál:
Na tomto tutoriálu začneme probírat logiky používané pro dokazování vlastností programů — Hoarovu logiku a separační logiku. Bude též probíráno, jakým způsobem mohou být tyto logiky reprezentovány v systému Coq a jak je možné použít Coq pro vytváření důkazů korektnosti programů v těchto logikách.
- 5. tutoriál:
Na tomto tutoriálu se seznámíme se základy typových systémů a problematikou dokazování vlastností těchto systémů.
- 6. tutoriál:
Poslední tutoriál bude věnován ukázkám toho, jak je možné Coq využít při dokazovánı́ vlastnostı́ funkcionálních programů a při verifikaci implementací datových struktur.
Řešení zadaných problémů
V průběhu semestru budou pravidelně zadávany úlohy k řešení jako domácí úkoly. Za řešení těchto úloh je možné získat až 15 bodů, přičem minimem nutným pro získání zápočtu je 7 bodů.
Důkaz korektnosti zadaného programu
Na konci semestru bude zadán jako domácí úkol problém vytvořit v systému Coq důkaz korektnosti jednoho celého programu. (Typicky se bude jednat o implementaci některého známého algoritmu.) Za tento důkaz korektnosti je možné získat až 20 bodů, přičemž nezbytné minimum je 10 bodů.
Podmínky pro získání zápočtu
Pro získání zápočtu je nutné získat za řešení problémů zadaných jako domácí úlohy a za vytvořený důkaz korektnosti zadaného programu v součtu minimálně 20 bodů (z celkového počtu 35 bodů).
Zkouška bude probíhat ústní formou. Za zkoušku je možné získat až 65 bodů. Nutné minimum bodů pro absolvování zkoušky je 30 bodů.
Výukové texty
Celý kurz je primárně postaven na následujícı́ sérii elektronických knih
Benjamin C. Pierce et al. — Software Foundations (volumes 1 – 6), Electronic textbook, 2022,
které jsou volně dostupné na webové adrese https://softwarefoundations.cis.upenn.edu.
Hlavním zdrojem budou především následující dvě knihy z této série:
- Volume 1: Logical Foundations — která se zabývá základy funkcionálnı́ho programovánı́ v Coqu a základy vytvářenı́ důkazů, tj. jakým způsobem je Coqu reprezentována výroková a predikátová logika, predikáty, funkce, důkazy indukcí, apod.
- Volume 2: Programming Language Foundations — která se zabývá základy sémantiky programovacı́ch jazyků, Hoarovou logikou a statickými typovými systémy, a tı́m, jak tyto věci reprezentovat v Coqu.
Stručně také budou probírána některá témata z následujících tří knih z této série:
- Volume 3: Verified Functional Algorithms — která se zabývá konkrétnı́mi přı́klady toho, jak dokazovat korektnost algoritmů reprezentovaných funkcionálnı́m způsobem v rámci jazyka Coqu. Tyto přı́klady zahrnujı́ napřı́klad třı́dı́cı́ algoritmy (Insertion Sort, Merge Sort, ...), implementaci různých datových struktur (např. různé druhy vyhledávacı́ch stromů, fronty, ...), barvenı́ grafu, apod.
- Volume 5: Verifiable C — která se zabývá tı́m, jakým způsobem je možné všechny dřı́ve popsané techniky dokazovánı́ korektnosti programů aplikovat na programy napsané v reálně použı́vaných nı́zkoúrovňových imperativnı́ch jazycı́ch, jako je jazyk C.
- Volume 6: Separation Logic Foundations — která se zabývá separačnı́ logikou.
Slidy
Zde se budou v průběhu semestru postupně objevovat slidy k tutoriálům pro školní rok 2022/2023.
- 1. tutoriál
Téma: Úvod. Základy funkcionálního programování v systému Coq.
Soubor se slidy: iadkp-01.pdf
- 2. tutoriál
Téma: Typový systém Coqu. Induktivně definované typy. Uživatelsky definované notace. Moduly. Polymorfismus. Logika.
Soubor se slidy: iadkp-02.pdf
- 3. tutoriál
Téma: Strukturování důkazů. Programování taktik. Induktivně definované relace. Sémantika programovacích jazyků.
Soubor se slidy: iadkp-03.pdf
- 4. tutoriál
Téma: Hoareova logika
Soubor se slidy: iadkp-04.pdf
- 5. tutoriál
Téma: Separační logika
Soubor se slidy: iadkp-05.pdf
Zadané úkoly
Ukázky kódu
Zde se budou v průběhu semestru postupně objevovat ukázky kódu v Coqu ilustrující některá probíraná témata.
- některé základní syntaktické konstrukce jazyka Coqu:
example_1.v- ukázka postupného vyhodnocování termu:
eval_add.v- příklad použití jazyka taktik ke zkrácení opakujícíchse podobných částí důkazu:
card_nat.v- složitější příklad použití jazyka taktik — naprogramování taktiky pro automatické dokázování toho, že jeden seznam je permutací druhého seznamu:
permut_list.v- implementace Hoareovy logiky — vychází z definic uvedených ve Volume 1 a Volume 2 Software Foundations (pozn.: některé definice byly drobně upraveny):
- hoare/LibMaps.v — implementace mapování názvů proměnných na jejich hodnoty
- hoare/LibImp.v — syntaxe a sémantika jednoduchého imperativního programovacího jazyka Imp
- hoare/LibAssertions.v — implementace assertions Hoareovy logiky
- hoare/LibHoare.v — definice základních pravidel Hoareovy logiky
- hoare/LibHoare2.v — definice programů anotovaných formulemi Hoareovy logiky
- hoare/Imp_examples.v — příklady sémantiky konkrétních jednoduchých programů v jazyce Imp
- hoare/Hoare_examples.v — příklady důkazů v Hoareově logice s použitím základních pravidel
- hoare/Hoare2_examples.v — příklady důkazů v Hoareově logice s použitím anotovaných programů
Další texty
- IADPK – studijní opora (autor: Zdeněk Sawa) — studijní opora k předmětu Interaktivnı́ a automatizované dokazovánı́ korektnosti programů pro kombinované
- Yves Bertot and Pierre Castéran: Interactive Theorem Proving and Program Development — Coq'Art: The Calculus of Inductive Constructions, Springer, 2004.
- Adam Chlipala: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, MIT Press, 2013.
Pozn.: Tato kniha je volně dostupná v elektronické podobě (jako PDF) na adrese http://adam.chlipala.net/cpdt/.- Andrew W. Appel et al.: Program Logics for Certified Compilers, Cambridge University Press, 2014.
- Hans Hüttel: Transitions and Trees: An Introduction to Structural Operational Semantics, Cambridge University Press, 2010.
- Benjamin C. Pierce: Types and Programming Languages, MIT Press, 2002.
- Benjamin C. Pierce, editor.: Advanced Topics in Types and Programming Languages, MIT Press, 2004.
- Glynn Winskel: Formal Semantics of Programming Languages, The MIT Press, 1993.