Master-Pflichtmodul MPM1: Formale Grundlagen der Informatik III (FGI-3)
Inhalt der Vorlesung "Semantik"
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 höhere Funktionen
- ein Konzept, das es typischerweise in imperativen Sprachen so nicht gibt.
Vortragsfolien
Benutzernamen und Passwort finden sich auf der kleinen Pinwand neben der Tür zu C-217.