1-INF-645 Teória programovania
Odporúčaný ročník: | 3. |
Semester: | zimný |
Rozsah: | K3 |
Hodnotenie: | 0/100 |
Počet kreditov: | 4 |
Vyučujúci: | prednáša RNDr. Igor Prívara CSc. cvičí RNDr. Dušan Guller PhD. |
www stránka: | |
Predmet je v tomto akademickom roku suspendovaný. |
Cieľ:
oboznámiť študentov so základnými témami teórie programovania: programové schémy a ich vlastnosti, správnosť programov a metódy dokazovania správnosti, formálna sémantikou programov a jazykov
Sylabus:
- 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, dokazovanie vlastností rekurzívnych programov
- systematický vývoj korektných 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 a rekurzívnych programov, typy a sémantika
- porovnávanie operačnej a denotačnej sémantiky - imperatívne programy, rekurzívne programy (korektnosť výpočtových pravidiel, kritériá korektnosti)
Literatúra:
Prívara, I.: Základy teórie programovania. Učebné texty (a priesvitky).