1-AIN-470 Špecifikácia a verifikácia programov

Novinky

Výučba tento semester

O kurze

Tu nájdete informačný list predmetu.

Cieľ predmetu

Predmet rozvíja schopnosti študentov uvažovať o správnosti programov, formálne špecifikovať požadované vlastnosti a dokazovať ich splnenie využitím rôznych metód, najmä štrukturálnej indukcie. Absolventi získajú znalosť konkrétnej formalizácie rekurzívnych programov, ich vlastností a dôkazov v jednoduchej logickej teórii Peanovej aritmetiky. Získajú tiež praktickú skúsenosť so špecifikáciou a verifikáciou väčšieho počtu programov.

Stručná osnova predmetu

Deklaratívne programovanie. Primitívna rekurzia. Rekurzia s mierou. Iteratívna rekurzia. Rekurzia na notácii. Párovacia funkcia a aritmetizácia. Štrukturálna rekurzia.

Špecifikačno-verifikačný systém. Peanova aritmetika. Matematická indukcia. Rozšírenia aritmetiky. Odvodené induktívne princípy: úplná matematická indukcia, indukcia s mierou, štrukturálna indukcia.

Dátové štruktúry. Reťazce. Zoznamy. Operácie na zoznamoch. Triedenie zoznamov. Aplikácie zoznamov. Binárne stromy. Binárne vyhľadávacie stromy. Aplikácie stromov. Symbolické výrazy. Interpreter programovacieho jazyka. Univerzálna funkcia.

Literatúra

J. Komara. Specification and Verification of Programs. Online.
Ján Kľuka. Úvod do deklaratívneho programovania. Online.

Výučba

* – aktualizované v priebehu posledných 7 dní

Posledná zmena: 2024-03-01T15:30+0100