Detail předmětu
Sémantika programovacích jazyků
SPJ Ak. rok 2012/2013 zimní semestr 3 kredity
Způsoby definice sémantiky programovacích jazyků: denotační, operační a axiomatická. Lambda kalkul a jeho použití pro denotační sématiku. Formální definice základních typů, struktur a konstrukcí denotační sématikou. Axiomatická sémantika a její použití pro dokazování programů. Příklad axiomatické definice jazyka. Sémantika jazyků pro funkcionální a logické programování.
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 26 hod. přednášky
Zajišťuje ústav
Získané dovednosti, znalosti a kompetence z předmětu
Schopnost formálně definovat sématiku programovacích jazyků a používat formální definice v praxi. Schopnost a praktické použití dokazování programů.
Cíle předmětu
Osvojit si teoretické základy pro definici sémantiky (významu) konstrukcí užívaných v programovacích jazycích. Získat schopnosti formálně tuto sémantiku definovat a formální definici používat.
Požadované prerekvizitní znalosti a dovednosti
Nejsou žádné prerekvizity.
Literatura studijní
- Češka, M., Motyčková, L., Hruška, T.: Vyčíslitelnost a složitost, skriptum VUT Brno, Ediční středisko VUT Brno 1992, 217 str., ISBN 80-214-0441-8
- Gordon, J.C.: Programming Language Theory and its Implementation, Prentice Hall - Series in Computer Science, Prentice Hall New York 1988, 255 str., ISBN 0-13-730409-9
Literatura referenční
- Gordon, J.C.: Programming Language Theory and its Implementation, Prentice Hall - Series in Computer Science, Prentice Hall New York 1988, 255 str., ISBN 0-13-730409-9
- Sebesta, R.,W.: Concepts of Programming Languages, Addison Wesley, Massachusetts 1999, 670 str., ISBN 9-780201-385960
Osnova přednášek
- Historie vývoje konstrukcí programovacích jazyků.
- Způsoby definice syntaxe a sémantiky.
- Základy netypovaného lambda kalkulu.
- Notace zápisu výrazů, vyhodnocování.
- Formální sémantika rekurzivních funkcí.
- Rozsahy platnosti jmen, typová kontrola.
- Datové typy jednoduché a strukturované, ekvivalence typů a polymorfizmus.
- Denotační sémantika.
- Floyd-Hoarova logika a její užití pro dokazování programů.
- Axiomatická sémantika a dokazování programů.
- Volání podprogramů a způsoby předávání parametrů.
- Objektově orientované programování.
- Funkcionální programování, logické programování.
Průběžná kontrola studia
Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.
Kontrolovaná výuka
Půlsemestrální test.