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.
