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
Unterlagen
Hier wird kapitelweise das Skript zum Download zur Verfügung stehen. Die Datumsangaben zeigen an, wann das entsprechende Kapitel zuletzt aktualisiert wurde.
| Skript PDF | ||
|---|---|---|
| 14.04.2010 | Organisation | Download |
| 14.04.2010 | Einführung | Download |
| 14.04.2010 | While-Syntax | Download |
| 20.04.2010 | Operationale Semantik für While | Download |
| 12.05.2010 | Compiler für While (Version 2) | Download |
| 18.05.2010 | Erweiterungen zu While - 1. Teil | Download |
| 25.05.2010 | Erweiterungen zu While - 2. Teil | Download |
| 08.06.2010 | Denotationale Semantik | Download |
| 08.06.2010 | Fixpunkttheorie | Download |
| 16.06.2010 | Adäquatheit und Kompositionalität | Download |
| 30.06.2010 | Continuations (Version 2) | Download |
| 22.07.2010 | Axiomatische Semantik (Version 2) | Download |
| 22.07.2010 | Gesamtes Skript (Version 2) | Download |
Termin
vom 14.04.2010, bis 14.07.2010
| Tag | Beginn | Ende | Ort |
|---|---|---|---|
| Mittwoch, 14.4.2010 | 14:00h | 15:30h | HS -101 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. Andreas Lochbihler |