Umiestnenie: Výučba | CL Homepage | KAI | FMFI UKBratislave

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

Novinky

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

Výučba


* – aktualizované v priebehu posledných 7 dní Posledná zmena: 2024-03-01T15:30+0100