IA011 Sémantiky programovacích jazyků

Fakulta informatiky
jaro 2021
Rozsah
2/1. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.
Vyučující
prof. RNDr. Antonín Kučera, Ph.D. (přednášející)
Mgr. Bc. Tomáš Janík (pomocník)
Garance
prof. RNDr. Antonín Kučera, Ph.D.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Antonín Kučera, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Čt 12:00–14:50 Virtuální místnost
Předpoklady
Předpokladem je znalost základních pojmů teorie množin a formální logiky (pravdivá a dokazatelná tvrzení, odvozovací systémy, korektnost a úplnost odvozovacích systémů, apod.)
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 48 mateřských oborů, zobrazit
Cíle předmětu
Úvodní kurs do teorie formálních sémantik programovacích jazyků, pokrývající základní paradigmata (operační, denotační, axiomatická) a vztahy mezi nimi. Okrajově jsou zmíněny další přístupy (temporalní logiky). Hlavním cílem kurzu je:
Výstupy z učení
Student bude:
chápat a rozlišovat definice formálních sémantik programovacích jazyků;
formálně argumentovat vlastnosti programů;
schopen číst a použít formule základní temporální logiky.
Osnova
  • Sémantiky programovacích jazyků, základní paradigmata (operační, denotanční a axiomatická sémantika).
  • Strukturální operační sémantika a její varianty. Ekvivalence sémantik.
  • Denotační sémantika. Pojem CPO, spojité funkce mezi CPO. Věta o pevném bodě a její aplikace, sémantika rekurze. Ekvivalence operační a denotanční sémantiky.
  • Axiomatická sémantika. Hoareův odvozovací systém, jeho korektnost a úplnost.
  • Temporální logiky, sémantika neukončených a paralelních programů.
Literatura
  • SCHMIDT, David A. The structure of typed programming languages. Cambridge: MIT Press, 1994, viii, 367. ISBN 0262193493. info
  • WINSKEL, Glynn. The formal semantics of programming languages : an introduction. Cambridge: MIT Press, 1993, xi, 361 s. ISBN 0-262-23169-7. info
Výukové metody
Přednášky, cvičení.
Metody hodnocení
Přednáška: 2 hodiny týdně. Cvičení: 1 hodina týdně.
Zkouška je písemná.
Informace učitele
http://www.fi.muni.cz/usr/kucera/teaching.html
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích podzim 2002, jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2022, jaro 2023, jaro 2024, jaro 2025.