Kurzus nemzetközi vendég- és részidős hallgatóknak

Kar

Informatikai Kar

Szervezet

IK Programozási Nyelvek és Fordítóprogramok Tanszék

Kód

IPM-22feszFSE

Cím

Formális szemantika Ea

Tervezett félév

Tavaszi

Meghirdetve

2024/25/2

ECTS

3

Nyelv

en

Oktatás célja

tudás: Komplex és aktuális ismeretekkel rendelkezik informatikai szakterületének innovatív, kutatói szintű műveléséhez szükséges általános, matematikai és számítástudományi elvek, szabályok, összefüggések terén, különösen a következő témakörökben: logika és alkalmazásai; a számítástudomány formális modelljei és eszközei. Átfogóan és naprakészen ismeri és érti az informatikai szakterületének általános elméleteit, összefüggéseit, tényanyagát és az ezekhez szükséges felépítő fogalomrendszert, különösen az alábbi területeken: verifikálás, programozási nyelvek, számítási modellek. Ismeri és érti a programozási nyelvek formális szemantikáinak megadásához és a ráépülő formális bizonyításokhoz használt matematikai fogalmakat és eszközöket. képesség: Képes matematikai, számítástudományi, informatikai ismereteinek, újszerű megközelítési módot igénylő alkalmazására informatikai kutatási, fejlesztési feladatok során. Képes egyszerű programozási nyelvek jelenségfogalmát formálisan definiálni, és azokra vonatkozóan nevezetes tételeket belátni. attitűd: Figyelemmel kíséri az informatikai szakterületével kapcsolatos szakmai, technológiai fejlődést. Elkötelezett a minőségi követelmények betartatására és informatikai eszközökkel történő elemzésére.

Tantárgy tartalma

A tárgy bemutatja a programozási nyelvek formális megadásakor használt fogalmakat és módszereket, különös tekintettel imperatív programozási nyelvek operációs (small-step, big-step) és denotációs szemantikáira. Tárgyalásra kerülnek a denotációs szemantikákban használt fixpont-elmélet alapjai és a szemantikákról való érvelésben használt indukciós bizonyítási módszerek. Vizsgáljuk programok ekvivalenciáját, valamint azt is, hogy a különböző módokon megadott szemantikák ekvivalensek-e egymással. A formális szemantikákat és a rájuk vonatkozó érveléseket gépi tételbizonyító rendszerben implementáljuk.

Számonkérés és értékelés

kollokvium

Irodalomjegyzék

Hanne Riis Nielson, Flemming Nielson: Semantics with Applications - An Appetizer (Springer-Verlag London) Benjamin C. Pierce et al. Software Foundations, Volume 2: Programming Language Foundations Kenneth Slonneger and Barry L. Kurtz: Formal Syntax and Semantics of Programming Languages (Addison Wesley Longman) Glynn Winskel: The Formal Semantics of Programming Languages - An Introduction (Foundations of Computing Series, MIT Press) John C. Reynolds: Theories of Programming Languages (Cambridge University Press)

Kurzus szakjai