Fakulta informačních technologií VUT v Brně

Detail předmětu

Sémantika programovacích jazyků

SPJ Ak. rok 2014/2015 zimní semestr 3 kredity

Předmět není v tomto roce otevřen
Zavřít
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

česky

Zakončení

zkouška (písemná)

Rozsah

26 hod. přednášky

Bodové hodnocení

70 zkouška, 30 půlsemestrální test

Zajišťuje ústav

Přednášející

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.

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

  1. Historie vývoje konstrukcí programovacích jazyků.
  2. Způsoby definice syntaxe a sémantiky.
  3. Základy netypovaného lambda kalkulu.
  4. Notace zápisu výrazů, vyhodnocování.
  5. Formální sémantika rekurzivních funkcí.
  6. Rozsahy platnosti jmen, typová kontrola.
  7. Datové typy jednoduché a strukturované, ekvivalence typů a polymorfizmus.
  8. Denotační sémantika.
  9. Floyd-Hoarova logika a její užití pro dokazování programů.
  10. Axiomatická sémantika a dokazování programů.
  11. Volání podprogramů a způsoby předávání parametrů.
  12. Objektově orientované programování.
  13. Funkcionální programování, logické programování.

Průběžná kontrola studia

Půlsemestrální test.

Zařazení předmětu ve studijních plánech

Nahoru