HOME | ENGLISH | IMPRESSUM | KIT

Semantik von Programmiersprachen

Aktuelles

DatumMitteilung
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.

Vorlesungsfortschritt

  • 24.4.2017: Bis einschließlich Abschnitt 2.1 (Syntax von While)

Ü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.

Übungsblätter

Übungsblätter PDF
24.04.2017 Übungsblatt 1 - Induktion 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