2-INF-123 Formálna sémantika a teória správnosti
| Odporúčaný ročník: | 1. |
| Semester: | zimný |
| Rozsah: | P3 |
| Hodnotenie: | 0/100 |
| Počet kreditov: | 6 |
| Vyučujúci: | prednáša RNDr. Igor Prívara CSc. |
| www stránka: |
Cieľ:
- analyzovať podstatné črty definície formálnej sémantiky programovacích jazykov s cieľom využiť ich pri návrhu PL
- charakterizovať a porovnávať rôzne sémantické definície daného programovacieho jazyka
- analyzovať zdravosť a úplnosť Hoareovských logických systémov vzhľadom na daný sémantický model (definovaný denotačne)
Sylabus:
- sémantika imperatívnych jazykov (základné príkazy, príkaz skoku, volanie rekurzívnej procedúry) - algebraická štruktúra sémantických domén, priama vs. "pokračovacia" sémantika (continuation)
- sémantika adresovania - sémantika blokov, modelovanie domén pre zložené dátové štruktúry
- sémantika beztypových funkcionálnych jazykov - lambda-kalkul, algebraická štruktúra domény), fixpointová sémantika, reflexívne domény, univerzálna doména
- sémantika nedeterministických konštrukcií - "relačná" fixpointová sémantika rekurzívnych procedúr, Egli-Milnerovo usporiadanie (aproximácia)
- vlastnosti Hoareovských systémov - zdravosť (korektnosť), resp. relatívna úplnosť systému
- najslabšia vstupná (wp) a najsilnejšia výstupná (sp) podmienka - syntaktická vs. sémantická charakterizácia, vyjadriteľnosť wp a sp
- porovnávanie operačnej, denotačnej a axiomatickej sémantiky
- typy v programovacích jazykoch - sémantika, typovacie pravidlá
Literatúra:
Milne,R., Strachey,Ch.: A Theory of Programming Language Semantics. Chapman & Hall, 1976
Winskel,G.: The Formal Semantics of Programming Languages. MIT Press, 1993
deBakker,J.: Mathematical Theory of Program Correctness. Prentice Hall, 1980
Zlatuška,J.: Lambda-kalkul. Masarykova Univerzita, 1993
Schmidt,D.A.: The Structure of Typed Programming Languages. MIT Press, 1994