Název:

Sémantika programovacích jazyků

Zkratka:SPJ
Ak.rok:2011/2012
Semestr:zimní
Studijní plán:
ProgramOborRočníkPovinnost
IT-MGR-2MBI-volitelný
IT-MGR-2MBS-volitelný
IT-MGR-2MGM-volitelný
IT-MGR-2MGM.-volitelný
IT-MGR-2MIN-volitelný
IT-MGR-2MIN.-volitelný
IT-MGR-2MIS2.povinně volitelný - skupina F
IT-MGR-2MIS.2.volitelný
IT-MGR-2MMI-volitelný
IT-MGR-2MMM-povinně volitelný - skupina L
IT-MGR-2MPS-volitelný
IT-MGR-2MPV-volitelný
IT-MGR-2MSK-volitelný
Vyučovací jazyk:čeština, angličtina
Kredity:3 kredity
Ukončení:zkouška (písemná)
Výuka:
hod./sempřednáškasem./cvičenílab. cvičenípoč. cvičeníjiná
Rozsah:260000
 zkouškatestycvičenílaboratořeostatní
Body:7030000
Garant:Hruška Tomáš, prof. Ing., CSc., UIFS
Přednášející:Hruška Tomáš, prof. Ing., CSc., UIFS
Křivka Zbyněk, Ing., Ph.D., UIFS
Fakulta:Fakulta informačních technologií VUT v Brně
Pracoviště:Ústav informačních systémů FIT VUT v Brně
Prerekvizity: 
Teoretická informatika (TIN), UITS
Nahrazuje:
Programovací jazyky (PRJ), UIFS
 
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.
Anotace:
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í.
Získané dovednosti, znalosti a kompetence:
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ů.
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í.
Literatura referenční:
  1. 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
  2. Sebesta, R.,W.: Concepts of Programming Languages, Addison Wesley, Massachusetts 1999, 670 str., ISBN 9-780201-385960
Literatura studijní:
  1. Č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
  2. 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
Průběžná kontrola studia:
Půlsemestrální test.