Aktuelles
| Datum | Mitteilung |
| 2.5.2017 | Web-App zur Visualisierung der Big- und Small-Step-Semantik aus der Vorlesung von J. Bechberger |
| – | Erste Vorlesung schon am 24.4.2017 zum Übungstermin |
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
- 24.4.2017: aktualisiertes Skript hochgeladen.
- 9.5.2017: Kapitel "Mathematische Grundlagen" hinzugefügt.
- 27.6.2017: Einige Kleinigkeiten verbessert (Schreibfehler, etc.).
- 24.7.2017: Noch mehr Kleinigkeiten verbessert.
Vorlesungsfortschritt
- 24.4.2017: Bis einschließlich Abschnitt 2.1 (Syntax von While)
- 25.4.2017: Bis zur Formulierung von Theorem 2 (Determinismus)
- 2.5.2017: Bis Ende Kapitel 3.3
- 9.5.2017: Bis Ende Kapitel 4.2 (Definition Compiler)
- 16.5.2017: Bis Ende Kapitel 4
- 23.5.2017: Bis zur Big-Step-Semantik für WhileX
- 30.5.2017: Bis Ende Kapitel 6.5 (Prozeduren)
- 13.6.2017: Bis Ende Kapitel 6 (Erweiterungen für While)
- 20.6.2017: Bis Mitte Kapitel 7.2 (Fixpunkttheorie, Definition von oberen Schranken)
- 27.6.2017: Bis Ende Kapitel 7.3 (Existenz des Fixpunkts für while)
- 4.7.2017: Bis Anfang Kapitel 7.5 (Continuation-style denotationale Semantik, Definition von 𝒞⟦_⟧)
- 11.7.2017: Bis Ende Kapitel 8.1 (Ein Korrektheitsbeweis mit der Denotationalen Semantik)
- 18.7.2017: Bis Ende Kapitel 8.6 (Semantische Prädikate und syntaktische Bedingungen)
- 25.7.2017: 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
- 16.6.2017: Beispiellösung Blatt 7 um eine vollständige Smallstep-Semantik für Parameterübergabe ergänzt.
Übungsblätter
| Übungsblätter PDF | ||
|---|---|---|
| 24.04.2017 | Übungsblatt 1 - Induktion | Download |
| 25.04.2017 | Übungsblatt 2 - Bigstep-Semantik | Download |
| 02.05.2017 | Übungsblatt 3 - Smallstep-Semantik | Download |
| 09.05.2017 | Übungsblatt 4 - Big- und Smallstep-Semantik | Download |
| 16.05.2017 | Übungsblatt 5 - Compiler | Download |
| 23.05.2017 | Übungsblatt 6 - Erweiterungen zu While | Download |
| 30.05.2017 | Übungsblatt 7 - Prozeduren | Download |
| 13.06.2017 | Übungsblatt 8 - Typsicherheit | Download |
| 20.06.2017 | Übungsblatt 9 - Denotationale Semantik | Download |
| 27.06.2017 | Übungsblatt 10 - Fixpunkttheorie | Download |
| 04.07.2017 | Übungsblatt 11 - Kontexte | Download |
| 11.07.2017 | Übungsblatt 12 - Continuations | Download |
| 18.07.2017 | Übungsblatt 13 - Axiomatische Semantik | Download |
| Beispiellösungen PDF | ||
| 05.04.2017 | Beispiellösung Übungsblatt 1 - Induktion | Download |
| 08.05.2017 | Beispiellösung Übungsblatt 2 - Bigstep-Semantik | Download |
| 15.05.2017 | Beispiellösung Übungsblatt 3 - Smallstep-Semantik | Download |
| 22.05.2017 | Beispiellösung Übungsblatt 4 - Big- und Smallstep-Semantik | Download |
| 29.05.2017 | Beispiellösung Übungsblatt 5 - Compiler | Download |
| 06.06.2017 | Beispiellösung Übungsblatt 6 - Erweiterungen zu While | Download |
| 12.06.2017 | Beispiellösung Übungsblatt 7 - Prozeduren | Download |
| 19.06.2017 | Beispiellösung Übungsblatt 8 - Typsicherheit | Download |
| 26.06.2017 | Beispiellösung Übungsblatt 9 - Denotationale Semantik | Download |
| 03.07.2017 | Beispiellösung Übungsblatt 10 - Fixpunkttheorie | Download |
| 10.07.2017 | Beispiellösung Übungsblatt 11 - Kontexte | Download |
| 17.07.2017 | Beispiellösung Übungsblatt 12 - Continuations | Download |
| 24.07.2017 | Beispiellösung Übungsblatt 13 - Axiomatische Semantik | Download |
| Übungsblätter Sourcecode | ||
| 25.04.2017 | Ableitungsbäume in Prolog | Download |
| 25.04.2017 | Auswertung arithmetischer und Bool’scher Ausdrücke in Prolog | Download |
| Beispiellösungen Sourcecode | ||
| 08.05.2017 | Prologimplementierung Bigstep | Download |
Termine
Vorlesung:
vom 24.04.2017, bis 29.07.2017
| Tag | Beginn | Ende | Ort |
|---|---|---|---|
| Montag, 24.4.2017 | 9:45h | 11:15h | SR -118, Geb. 50.34 |
| Dienstag | 11:30h | 13:00h | SR 301, Geb. 50.34 |
Übung:
vom 08.05.2017, bis 29.07.2017
| Tag | Beginn | Ende | Ort |
|---|---|---|---|
| Montag | 9:45h | 11:15h | SR -118, Geb. 50.34 |
| Dienstag, 6.6.2017 | 11:30h | 13:00h | SR 301, Geb. 50.34 |
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
| Ehemalige Mitarbeiter |
|---|
| Dr.-Ing. Sebastian Ullrich |
| Dipl.-Inform. Denis Lohner |