Předmět je základní jednotka výuky, jejímž prostřednictvím si student osvojí ucelenou část souboru znalostí a dovedností, potřebnou pro zvládnutí studijního oboru/specializace. Za věcný obsah předmětu zodpovídá garant předmětu. Časovou náročnost předmětu zhruba vyjadřuje atribut předmětu rozsah kontaktní výuky. Například rozsah = 2+2 značí, že předmět bude mít týdně dvě hodiny přednášek a dvě hodiny cvičení týdně. Na závěr semestru musí vyučující provést vyhodnocení, nakolik si ten který student osvojil poznatky a dovednosti, kterých měl během výuky nabýt. Jakým způsobem toto hodnocení vyučující provedou určuje atribut způsob zakončení. U předmětu lze definovat, že předmět je zakončen pouze zápočtem(Z), klasifikovaným zápočtem(KZ), pouze zkouškou(ZK), nebo zápočtem a zkouškou(Z,ZK). Náročnost úspěšného absolvování předmětu je vyjádřena ECTS kreditními body. Výuka předmětu probíhá během semestru. Opakovaně se předmět vyučuje vždy v zimním(Z), nebo v letním(L) semestru každého akademického roku. Výjimečně může předmět být nabízen studentům v obou semestrech(Z,L). Za organizační zajištění výuky zodpovídá přiřazená katedra, která zejména vytvoří časový rozvrh předmětu a zajistí pro předmět vyučující. Někteří přednáší a zkouší, jiní vedou cvičení a udělují zápočty.
Obsahová náplň a další organizační informace, týkající se předmětu je popsána pomocí různých popisných textů(anotace, týdenní osnova, literatura, apod.)
$DODATEK_POPIS
NI-FME | Formální metody a specifikace | Rozsah kontaktní výuky: | 2P+1C | ||
---|---|---|---|---|---|
Vyučující: | Ratschan S. | Způsob zakončení: | Z,ZK | ||
Zodpovědná katedra: | 18102 | ECTS Kredity: | 5 | Semestr: | L |
Anotace:
Studenti dokážou formálně popisovat sémantiku programů a používat logické uvažování pro konstrukci správně fungujícího programu. Naučí se principy softwarových nástrojů, které slouží k dokazování základních vlastností algoritmů.
Osnovy přednášek:
1. | Úvod do formální specifikace programů. | |
2. | Dokazovací metody. | |
3. | Logické teorie a modelování datových struktur. | |
4. | Operační sémantika programů. | |
5. | Ověření omezené správnosti programů. | |
6. | Ověření neomezené správnosti programů. | |
7. | Funkce, procedury. | |
8. | Důkazy terminace. | |
9. | Symbolické provádění. | |
10. | Rozhodovací procedury. | |
11. | Objektově orientované programování. | |
12. | Syntéza programů. |
Osnovy cvičení:
Cvičení materiálu z přednášky.
Literatura:
1. | Clarke, E.M. - Henzinger, Th.A. - Veith, H. - Bloem, R. (Eds.) : Handbook of Model Checking. Springer, 2018. ISBN 978-3-319-10574-1. | |
2. | Kroening, D. - Strichman, O. : Decision Procedures - An Algorithmic Point of View, 2nd edition. Springer, 2016. ISBN 978-3-662-50496-3. | |
3. | Bradley, A. R. - Manna, Z. : The Calculus of Computation. Springer, 2007. ISBN 978-3-540-74113-8. |
Požadavky:
Znalost základních pojmů matematické logiky a teorie množin, schopnost je používat.
|
Předmět je zahrnut do těchto studijních plánů:
Stránka vytvořena 19. 4. 2024, semestry: Z/2021-2, Z/2023-4, Z/2022-3, Z/2019-20, Z/2024-5, L/2021-2, L/2020-1, L/2022-3, L/2023-4, Z/2020-1, L/2019-20, připomínky k informační náplni zasílejte správci studijních plánů | Návrh a realizace: J. Novák, I. Halaška |