Zpět

Interaktivní a automatizované dokazování korektnosti programů

Garant, přednášející, cvičící i tutor pro studenty v kombinované formě studia:

Aktuální informace

Zde se budou v průběhu semestru objevovat aktuální informace týkající se předmětu IADKP.

Náplň předmětu

Předmět v sobě kombinuje několik témat:

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:

  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. Ekvivalence programů.
  8. Logika pro dokazovánı́ vlastnostı́ programů — Hoarova logika.
  9. Separačnı́ logika.
  10. Typové systémy. Dokazovánı́ vlastnostı́ typových systémů.
  11. Dokazovánı́ vlastnostı́ funkcionálnı́ch programů.

Předběžný program tutoriálů:

Požadavky na zápočet

Ř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

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

Materiály

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:

Stručně také budou probírána některá témata z následujících tří knih z této série:

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

Zde se budou v průběhu semestru postupně objevovat zadané úkoly pro školní rok 2022/2023.

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

Další texty

Další literatura

Zpět