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

Detail předmětu

Programovací jazyky

PRJ Ak. rok 2004/2005 letní semestr 6 kreditů

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í. Základy objektového programování.

Garant předmětu

Jazyk výuky

česky

Zakončení

zápočet+zkouška (písemná)

Rozsah

39 hod. přednášky, 12 hod. cvičení, 14 hod. projekty

Bodové hodnocení

50 zkouška, 20 půlsemestrální test, 30 projekty

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. Seznámit se se základními modely programovacích jazyků.

Požadované prerekvizitní znalosti a dovednosti

teoretická informatika, formální jazyky

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

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í.
  • Rekurzivní funkce.
  • Rozsahy platnosti jmen, typová kontrola.
  • Datové typy jednoduché a strukturované, ekvivalence typů a polymorfizmus.
  • Denotační sémantika.
  • Floyd-Hoarova logika.
  • 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í.

Osnova numerických cvičení

  • Základní konstrukce a operace lambda kalkulu.
  • Reprezentace základních typů v lambda kalkulu.
  • Reprezentace strukturovaných typů v lambda kalkulu.
  • Denotační sémantika jednoduchého jazyka.
  • Základy Floyd-Hoareovy logiky.
  • Dokazování programů.

Osnova ostatní - projekty, práce

  • Realizace části sémantické analýzy překladačů různých jednoduchých jazyků v kombinaci s projektem v předmětu Základy překladačů.

Průběžná kontrola studia

Test v polovině semestru. Průběžná kontrola řešení projektu vedoucím.

Kontrolovaná výuka

Účast na numerických cvičeních. Jde o 14 denní cyklus. Je možné se mimořádně účastnit v druhém týdnu.

Podmínky zápočtu

Nejméně polovina bodů, které lze získat za aktivity během semestru (testy a projekt), tj. 25 bodů.
Nahoru