Aktuelles
| Datum | Mitteilung |
| 8.7.2015 | In der letzten Vorlesungswoche findet sowohl am Montagstermin (13.7.) als auch am Mittwochstermin (15.7.) Vorlesung statt. |
| – | Erste Vorlesung schon am 13.4.2015 zum Übungstermin |
Semantik von Programmiersprachen
Die formale Semantik einer Programmiersprahce 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
- Diplom-Studenten
- Diese Veranstaltung ist Teil der Vertiefungsfächer
- VF 1: Theoretische Grundlagen
- VF 6: Softwaretechnik und Übersetzerbau
- Master-Studenten
- Diese Veranstaltung ist Teil der Module
- IN4INSPT Sprachtechnologien
- IN4INFM Formale Methoden
Skript
Das Semantik-Skript wurde von Andreas Lochbihler erstellt und wird von uns weiter überarbeitet. Größere Änderungen werden hier erwähnt. Darüber hinaus wird angebeben, wie weit wir jeweils in der Vorlesung gekommen sind.
Änderungen
- 17.3.2015: Skript hochgeladen.
- 6.5.2015: Kleine Vereinfachung des Beweises des Aufteilungslemmas (Lemma 16).
- 20.5.2015: Variation der Big-Step-Semantik für WhileX.
- 16.7.2015: Ergänzung Bonuskapitel 8.
- 16.7.2015: Beispiele und Definitionen werden jetzt wie gewünscht gemeinsam mit Lemmas und Theoremen hochgezählt.
Vorlesungsfortschritt
- 13.4.2015: Bis einschließlich Abschnitt 2.1 (Syntax von While)
- 15.4.2015: Bis zur Formulierung von Theorem 2 (Determinismus)
- 22.4.2015: Bis zur Formulierung von Lemma 7 (Zerlegungslemma für Sequenz)
- 29.4.2015: Bis zu Definition 11 (Compiler)
- 6.5.2015: Bis Ende Kapitel 4
- 13.5.2015: Bis zur Small-Step-Semantik für WhileX
- 20.5.2015: Bis Ende Kapitel 5.5 (Prozeduren)
- 27.5.2015: Bis einschließlich Lemma 24 (Erhalt der Zustandskonformanz)
- 3.6.2015: Bis Ende Kapitel 6.1 (Definition der denotationalen Semantik)
- 10.6.2015: Bis Ende Kapitel 6.2 (Fixpunkttheorie)
- 17.6.2015: Bis Ende Kapitel 6.4 (Bezug zur Operationalen Semantik)
- 24.6.2015: Bis Ende Kapitel 6 (Denotationale Semantik)
- 1.7.2015: Bis Ende Kapitel 7.3 (Inferenzregeln für While)
- 8.7.2015: Bis Ende Kapitel 7.6 (Semantische Prädikate und syntaktische Bedingungen)
- 13.7.2015: Bis Ende Kapitel 7.7 (Verifikationsbedingungen)
- 15.7.2015: Bonuskapitel 8 (Semantik von Funktionalen Programmiersprachen)
Ü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. selbsständig, z.T. gemeinsam in der Übung gelöst werden. Im Anschluss wird hier eine Musterlösung veröffentlicht.
Übungsblätter
| Übungsblätter PDF | ||
|---|---|---|
| 13.04.2015 | Übungsblatt 1 - Induktion | Download |
| 15.04.2015 | Übungsblatt 2 - Bigstep-Semantik | Download |
| 22.04.2015 | Übungsblatt 3 - Smallstep-Semantik | Download |
| 29.04.2015 | Übungsblatt 4 - Big- und Smallstep-Semantik | Download |
| 06.05.2015 | Übungsblatt 5 - Compiler | Download |
| 13.05.2015 | Übungsblatt 6 - Erweiterungen zu While | Download |
| 20.05.2015 | Übungsblatt 7 - Prozeduren | Download |
| 27.05.2015 | Übungsblatt 8 - Typsicherheit | Download |
| 03.06.2015 | Übungsblatt 9 - Denotationale Semantik | Download |
| 10.06.2015 | Übungsblatt 10 - Fixpunkttheorie | Download |
| 17.06.2015 | Übungsblatt 11 - Kontexte | Download |
| 24.06.2015 | Übungsblatt 12 - Continuations | Download |
| 06.07.2015 | Übungsblatt 13 - Axiomatische Semantik | Download |
| Übungsblätter Sourcecode | ||
| 15.04.2015 | Auswertung arithmetischer und Bool’scher Ausdrücke in Prolog | Download |
| 20.04.2015 | Ableitungsbäume in Prolog | Download |
Termine
Vorlesung:
vom 13.04.2015, bis 15.07.2015
| Tag | Beginn | Ende | Ort |
|---|---|---|---|
| Montag, 13.4.2015 | 9:45h | 11:15h | SR 236, Geb. 50.34 |
| Mittwoch | 14:00h | 15:30h | SR 236, Geb. 50.34 |
Übung:
vom 20.04.2015, bis 13.07.2015
| Tag | Beginn | Ende | Ort |
|---|---|---|---|
| Montag | 9:45h | 11:15h | SR 236, 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
Veranstalter
| Lehrstuhlinhaber |
|---|
| Prof. Gregor Snelting |
| Ehemalige Mitarbeiter |
|---|
| Dr. rer. nat. Joachim Breitner |
| Dipl.-Inform. Denis Lohner |