HOME | ENGLISH | IMPRESSUM | KIT

Semantik von Programmiersprachen

Aktuelles

DatumMitteilung
2.5.2017Web-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

Wissenschaftliche Mitarbeiter
Denis Lohner
Sebastian Ullrich