Zuerst stellen wir, nach einigen motivierenden Beispielen und einer knappen Übersicht, die ordnungstheoretischen Grundlagen der denotationellen Semantik bereit.
Dann zeigen wir, wie man formal eine denotationelle Semantik für eine
funktionale bzw. eine prozedurale Sprachen entwickeln kann und wie die Art der semantischen Beschreibung u.a. von der Gestalt der Sprache und den verwendeten Konzepten abhängt.
Als nächstes erklären wir anhand des Spezialfalles D = [D -> D] was mit einem rekursiven semantischen Bereich "gemeint" ist.
Schließlich widmen wir uns noch der Programmverifikation.
Hier studieren wir einige Methoden, die auch zur Programmentwicklung vewendet werden können.
Bei den funktionalen Sprachen behandeln wir Fixpunkt-Verifikationsmethoden.
Verifikation von prozeduralen Programmen führt hingegen zur axiomatischen Semantik.
Hier behandeln wir die beiden bekanntesten Ausprägungen, nämlich den
Hoare-Kalkül für partielle und den wp-Kalkül für totale Korrektheit.
Falls Zeit bleibt, so gehen wir noch auf weitere Anwendungen der Semantik von Programmiersprachen ein, etwa auf transformationelle Programmierung oder formale Korrektheitsbeweise von Übersetzern.
Die Vorlesung orientiert sich an dem Buch "Semantik von
Programmiersprachen" von R. Berghammer, welches im Jahr 2001 beim
Logos-Verlag erschienen ist.
