Odporúčaný ročník: | 3. |
Semester: | letný |
Rozsah: | K4 |
Hodnotenie: | 40/60 |
Počet kreditov: | 4 |
Vyučujúci: | prednáša RNDr. Igor Prívara CSc. |
www stránka: |
Absolvent si osvojí: princípy abstrakcie programov s cieľom analyzovať vlastnosti riadiacich štruktúr programov, nezávislé od konkrétnej interpretácie programu, princípy a metódy dokazovania správnosti programov, základné poznatky potrebné pre formálnu definíciu významu (sémantiky) impreratívnych a rekurzívnych programovacích jazykov.
Programové schémy: základné pojmy - štandardná schéma, interpretácia schémy, Herbrandove interpretácie, vlastnosti schém; rozhodnuteľnosť základných vlastností schém – základné výsledky o nerozhodnuteľnosti, podtriedy schém s rozhodnuteľnými vlastnosťami (voľné, Janovove schémy); porovnávanie a preklad tried schém - vzťahy medzi triedami štandardných, štruktúrovaných a rekurzívnych schém, čiastočne interpretované schémy.
Správnosť programov: čiastočná a totálna správnosť - invarianty a induktívne formuly, najslabšia vstupná a najsilnejšia výstupná podmienka; metódy dokazovania – Floydova metóda, Hoareovský dokazovací systém, indukčné techniky; systematický vývoj správnych programov.
Sémantika programov a jazykov: význam programu - princípy operačnej, denotačnej a axiomatickej sémantiky, sémantické domény – algebraická štruktúra, konštrukcia domén; formálna sémantika (operačný a denotačný význam) imperatívnych programov, porovnávanie operačnej a denotačnej sémantiky imperatívnych programov; formálna sémantika (operačný a denotačný význam) rekurzívnych funkcionálnych programov, porovnávanie operačnej a denotačnej sémantiky rekurzívnych programov, dokazovanie vlastností rekurzívnych programov.
Matematická teorie programů / Zohar Manna ; z amerického originálu přeložil Jiří Hořejš. Praha : Státní nakladatelství technické literatury, 1981
Prívara, I.: Úvod do teórie programovania, Učebné texty (verzia 2014 – pdf)