HOME | ENGLISH | IMPRESSUM | KIT

Semantik von Programmiersprachen

Aktuelles

DatumMitteilung
8.7.2015In 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
ECTS-Punkte: 4

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
Wissenschaftliche Mitarbeiter
Denis Lohner
Ehemalige Mitarbeiter
Dr. rer. nat. Joachim Breitner