Semantik von Programmiersprachen (original) (raw)

Aktuelles

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. Parallel dazu gibt es eine Übung, in der die Inhalte der Vorlesung angewandt und vertieft werden.

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

Unterlagen

Hier wird kapitelweise das Skript zum Download zur Verfügung stehen. Die Datumsangaben zeigen an, wann das entsprechende Kapitel zuletzt aktualisiert wurde.

Termin

vom 17.04.2012, bis 18.07.2012

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