Detail předmětu

Sémantika programovacích jazyků

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

Aktuální akademický rok

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

Hruška Tomáš, prof. Ing., CSc. (UIFS)

Jazyk výuky

česky

Zakončení

zkouška

Rozsah

  • 26 hod. přednášky

Zajišťuje ústav

Ústav informačních systémů (UIFS)

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

  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

Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.

Metody vyučování

Výuka předmětu je realizována formou: Přednáška - 2 vyučovací hodiny týdně.

Kontrolovaná výuka

Půlsemestrální test.

Nahoru