Aktuelles
| Datum | Mitteilung |
| 2.9.2021 | Für den Prüfungstermin am 15.9.2021 fehlt uns noch die Bestätigung, bitte UNBEDINGT beim Sekretariat melden! |
| 4.6.2019 | Der Übungstermin am 10.6. entfällt wegen Pfingsten und wird am Freitag, den 14.6.2019 um 14:00 nachgeholt. Ort ist wie immer der SR-118. |
Semantik von Programmiersprachen
Die formale Semantik einer Programmiersprache beschreibt mit mathematischen Mitteln, was die exakte Bedeutung eines Programms bzw. der Ablauf des Programms während seiner Ausführung ist.
Erst mittels einer solchen Semantik kann man eine Programmiersprache exakt beschreiben, wobei man gleichzeitig ein Verständnis für die Feinheiten der Programmiersprache entwickelt.
Außerdem braucht man eine Semantik, um überhaupt Aussagen über Programme, die Programmiersprache oder Programmanalysen mathematisch formulieren und als korrekt nachweisen zu können.
Ein Beispiel dazu wäre die Sicherheitseigenschaft, dass ein Programm nicht wegen illegaler Casts abstürzen kann.
In dieser Vorlesung werden die mathematischen Grundlagen formaler Semantik zusammen mit Anwendungen vorgestellt.
Themen
-
Abstrakte Syntax
-
Operationale Semantik
-
Grundlagen von Typsystemen und Typsicherheit
-
Denotationale Semantik
-
Continuation-Semantik
-
Axiomatische Semantik und Korrektheit des Hoare-Kalküls
Voraussetzungen
Kenntnisse mit formalen Beschreibungen (Vorlesung Formale Systeme) sind sehr vorteilhaft.
Einordnung
- Master-Studenten (SPO 2008 & 2015)
- Diese Veranstaltung wird als eigenständiges Modul angeboten: M-INFO-100845.
ECTS-Punkte: 4
Skript
Das Semantik-Skript wurde von Andreas Lochbihler erstellt, im SS 2015 von Joachim Breitner ergänzt, und wird von uns weiter überarbeitet. Größere Änderungen werden hier erwähnt. Darüber hinaus wird angegeben, wie weit wir jeweils in der Vorlesung gekommen sind.
Änderungen
- 23.4.2019: Kapitel 1.3: Beispiel der operationalen Semantik an spätere Notation angepasst.
- 3.5.2019: Ein Versuch, Variablen konsistenter von 1 ausgehend durchzuzählen
- 21.5.2019: Prosa-Erklärung zum Aufteilungslemma hinzugefügt, JmpFT-Regel zu JmpTT umbenannt
- 28.5.2019: Übungsaufgabe zu WhileBlock hinzugefügt
- 4.6.2019: Syntax der BigStep-Semantik mit Prozeduren geändert: E jetzt rechts vom Turnstile
- 9.7.2019: Variablen in Theorem 128 etwas sinnvoller benannt
Vorlesungsfortschritt
- 23.4.2019: Bis einschließlich Abschnitt 3.1 (Syntax von While)
- 30.4.2019: Bis zur Formulierung von Theorem 10 (Determinismus)
- 7.5.2019: Bis einschließlich Lemma 19
- 14.5.2019: Bis Ende Kapitel 5.2 (Definition Compiler)
- 21.5.2019: Bis Ende Kapitel 5
- 28.5.2019: Bis einschließlich Lemma 46
- 5.6.2019: Bis Ende Kapitel 6.5 (Prozeduren)
- 11.6.2019: Bis Ende Kapitel 6 (Erweiterungen für While)
- 18.6.2019: Bis Mitte Kapitel 7.2 (Fixpunkttheorie, Definition von oberen Schranken)
- 25.6.2019: Bis Ende Kapitel 7.2 (Knaster-Tarski-Fixpunktsatz)
- 2.7.2019: Bis Ende Kapitel 7.4 (Bezug zur operationalen Semantik)
- 9.7.2019: Bis Ende Kapitel 8.1 (Ein Korrektheitsbeweis mit der Denotationalen Semantik)
- 16.7.2019: Bis Ende Kapitel 8.6 (Semantische Prädikate und syntaktische Bedingungen)
- 23.7.2019: Bis Ende Kapitel 8 (Axiomatische Semantik)
Übung
Parallel dazu gibt es eine Übung, in der die Inhalte der Vorlesung angewandt und vertieft werden. Dazu erscheint jede Woche ein Übungsblatt mit Aufgaben, die z.T. selbstständig, z.T. gemeinsam in der Übung gelöst werden. Im Anschluss wird hier eine Beispiellösung veröffentlicht.
Änderungen
- 8.5.2019: Hinweis zu ÜB 3 Aufgabe 2 ergänzt, Blatt veröffentlicht.
- 13.5.2019: Fehler in Aufgabe 1 auf Blatt 3 verbessert, Lösung veröffentlicht.
Übungsblätter
| Übungsblätter Sourcecode |
| 30.04.2019 |
common.pl |
Download
|
| 06.05.2019 |
bigstep.pl |
Download
|
| 06.05.2019 |
derivTree.pl |
Download
|
| Übungsblätter PDF |
| 26.04.2019 |
Übungsblatt 1 - Induktion |
Download
|
| 30.04.2019 |
Übungsblatt 1 (Lösung)- Induktion |
Download
|
| 30.04.2019 |
Übungsblatt 2 - Big-Step |
Download
|
| 06.05.2019 |
Übungsblatt 2 (Lösung) - Big-Step |
Download
|
| 08.05.2019 |
Übungsblatt 3 - Small-Step |
Download
|
| 13.05.2019 |
Übungsblatt 3 (Lösung) - Small-Step |
Download
|
| 16.05.2019 |
Übungsblatt 4 - Big-Step und Small-Step |
Download
|
| 20.05.2019 |
Übungsblatt 4 (Lösung) - Big-Step und Small-Step |
Download
|
| 21.05.2019 |
Übungsblatt 5 - Compiler |
Download
|
| 28.05.2019 |
Übungsblatt 5 (Lösung) - Compiler |
Download
|
| 28.05.2019 |
Übungsblatt 6 - Erweiterungen zu While |
Download
|
| 03.06.2019 |
Übungsblatt 6 (Lösung) - Erweiterungen zu While |
Download
|
| 05.06.2019 |
Übungsblatt 7 - Prozeduren |
Download
|
| 11.06.2019 |
Übungsblatt 8 - Typsicherheit |
Download
|
| 17.06.2019 |
Übungsblatt 7 (Lösung) - Prozeduren |
Download
|
| 17.06.2019 |
Übungsblatt 8 (Lösung) - Typsicherheit |
Download
|
| 18.06.2019 |
Übungsblatt 9 - Denotationale Semantik |
Download
|
| 24.06.2019 |
Übungsblatt 9 (Lösung) - Denotationale Semantik |
Download
|
| 25.06.2019 |
Übungsblatt 10 - Fixpunkttheorie |
Download
|
| 02.07.2019 |
Übungsblatt 10 (Lösung) - Fixpunkttheorie |
Download
|
| 02.07.2019 |
Übungsblatt 11 - Kontexte |
Download
|
| 09.07.2019 |
Übungsblatt 11 (Lösung) - Kontexte |
Download
|
| 09.07.2019 |
Übungsblatt 12 - Continuations |
Download
|
| 15.07.2019 |
Übungsblatt 12 (Lösung) - Continuations |
Download
|
| 22.07.2019 |
Übungsblatt 13 - Axiomatische Semantik |
Download
|
| 22.07.2019 |
Übungsblatt 13 (Lösung) - Axiomatische Semantik |
Download
|
Termine
Vorlesung:
Die Vorlesung findet immer dienstags um 15:45 im Seminarraum 301 statt.
| Tag | Datum | Beginn | Ende | Ort |
|---|
| Dienstag | 23.04.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 30.04.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 07.05.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 14.05.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 21.05.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 28.05.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 04.06.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 11.06.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 18.06.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 25.06.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 02.07.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 09.07.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 16.07.2019 | 15:45 | 17:15 | Raum 301 |
| Dienstag | 23.07.2019 | 15:45 | 17:15 | Raum 301 |
Übung:
Die Übung findet immer montags um 14:00 im Seminarraum -118 statt. In der ersten Vorlesungswoche
und am Pfingstmontag ist keine Übung.
| Tag | Datum | Beginn | Ende | Ort |
|---|
| Montag | 29.04.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 06.05.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 13.05.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 20.05.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 27.05.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 03.06.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 17.06.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 24.06.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 01.07.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 08.07.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 15.07.2019 | 14:00 | 15:30 | Raum -118 |
| Montag | 22.07.2019 | 14:00 | 15:30 | Raum -118 |
Literatur
-
Hanne Riis Nielson, Flemming Nielson.
Semantics with Applications: An Appetizer.
Springer Verlag, 2007. Zweite Auflage.
ISBN: 978-1-84628-691-9.
Grundlage der meisten Themen der Vorlesung, sehr anschaulich und gut verständlich.
-
John C. Reynolds.
Theories of Programming Languages.
Cambridge University Press, 1998.
ISBN: 0-521-59414-6.
Fokus auf denotationaler Semantik
-
Benjamin C. Pierce. Types and Programming Languages.
MIT Press, 2002. ISBN: 0-262-162209-1.
Schwerpunkt auf dem Lamda-Kalkül und Typsystemen, mit sehr guten Erklärungen, auch zu weiterführenden Themen.
-
Glynn Winskel.
The Formal Semantics of Programming Languages. An Introduction.
MIT Press, 1993.
ISBN: 0-262-73103-7.
Ausführlicher Beweis der Unentscheidbarkeit eines vollständigen axiomatischen Kalküls
-
Tobias Nipkow, Gerwin Klein.
Concrete Semantics.
Springer, 2014.
ISBN: 978-3-319-10542-0.
http://www.concrete-semantics.org/
Formalisierung des Vorlesungsstoffs im Theorembeweiser Isabelle, inklusive einer Einführung in diesen.
Veranstalter
