Master-Modul MPM1: Semantik
Formale Grundlagen der Informatik III (FGI-3)

Eine Hauptaufgabe der Semantik von Programmsprachen besteht also darin, implementationsunabhängige, in sich konsistente Definitionen von Syntax und Semantik zu finden. Beispielsweise enthielten frühe Definitionen von Programmsprachen keine Konzepte für Ein- und Ausgabe, da diese zu abhängig vom jeweils benutzten Rechner waren. Gesichtspunkte der Migration, Kooperation und Erlernbarkeit erfordern auch hier einheitliche Konzepte.

Die Vorlesung umfasst vier große Blöcke:

• Semantik imperativer Programmsprachen. Fundamentale Ansätze sind die operationale und die denotationale Semantik.
• Axiomatische Semantik, die ein Kalkül zur syntaxorientierten Form der Programmverifikation bereitstellt.
• Die Theorie abstrakter Datentypen, bei der das Konzept der Syntax insofern erweitert wird, als dass axiomatisch die Gültigkeit einer Menge von Gleichungen gefordert wird.
• Lambda-Kalkül und Typtheorie stellen die Grundlage funktionaler Programmiersprachen dar. Typtheorie studiert insbesondere Funktionen höherer Ordnung - ein Konzept, das es typischerweise in imperativen Sprachen so nicht gibt.

Skript

• Skript zur Vorlesung [1.6 Mb]

Vortragsfolien

• Denotationale Semantik
• Axiomatische Semantik
• Arrays und Abbruch
• Operationale Semantik
• Reduktionssysteme
• Der Lambda-Kalkül
• Abstrakte Datentypen