Modulcode:	Inf-SemPS
Englische Bezeichnung:	Semantics of Programming Languages
Modulverantwortliche(r):	Prof. Dr. Rudolf Berghammer
Turnus:	unregelmäßig (SS11 WS12/13 SS14 SS15 SS17)
Präsenzzeiten:	4V 2Ü
ECTS:	8
Workload:	240 Std.
Dauer:	ein Semester
Modulkategorien:	TI (MSc Inf (15)) WI (MSc Inf (15)) WI (MSc WInf (15)) WI (MEd Inf) WPI (MEd Inf) TG (MSc Inf) MV (MSc Inf)
Lehrsprache:	Deutsch
Voraussetzungen:

Kurzfassung:

Eine präzise Beschreibung der Bedeutung von Programmen ist eine unerläßliche Voraussetzung für viele Dinge, die Programmiersprachen und Programmierung betreffen. Diese Vorlesung befaßt sich mit der formalen, d.h. mit mathematischen Methoden durchgeführten, semantischen Beschreibung der Kontrollstrukturen von Programmiersprachen und einigen Anwendungen in der Programmverifikation und Programmentwicklung.

Lernziele:

Als das hauptsächliche Ziel will die Vorlesung die in der theoretischen Informatik zur Zeit bedeutendsten Methoden zur Formalisierung der Semantik der Kontrollstrukturen einer Programmiersprache vermitteln, wobei sie sich auf sogenannte sequentielle Sprachen beschränkt, also keine parallelen oder verteilten Abläufe betrachtet. Die Vermittlung von Methoden beinhaltet auch die dazu notwendigen Grundlagen und bezieht sich somit konsequenterweise auch auf den mathematischen Hintergrund. Bei der Darstellung dieses Stoffs wird versucht, die Gegenstände, etwa die Programmiersprachen bei den verschiedenen Semantikfestlegungen, so einfach wie möglich zu halten, damit die verwendeten Methoden und die Zusammenhänge nicht durch einen übermäßigen technischen Aufwand verdeckt werden. Auch auf eine ausführliche Beweisführung wird großer Wert gelegt. Und schließlich soll als Anwendung von Semantik noch gezeigt werden, wie wissenschaftliche Methoden zur Programmentwicklung sich auf diese semantischen Grundlagen stützen können. Aus Umfangsgründen wird dabei der Schwerpunkt auf das begriffliche Gerüst gelegt und es werden folglich nur kleinere und übersichtliche Beispiele behandelt.

Lehrinhalte:

Die Lerninhalte ergeben sich ungefähr aus der nachfolgend angegebenen voraussichtlichen Gliederung der Vorlesung.

• Beispiele für semantische Fragestellungen
• Mathematische Grundlagen von Semantik
• Denotationelle Semantik funktionaler Programmiersprachen
• Denotationelle Semantik imperativer Programmiersprachen
• Lösung von Bereichsgleichungen
• Programmverifikation und axiomatische Semantik

Weitere Voraussetzungen:

Kenntnisse über Programmiersprachen und deren Anwendungen, die insbesondere in den Vorlesungen der ersten beiden Studienjahre erworben werden können. Weiterhin wird erwartet, daß auch die Mathematikkenntnisse dieses Bereichs des Studiums vorhanden sind, insbesondere jene, welche Funktionen, Ordnungen, Induktionsmethoden und Logik betreffen.

Prüfungsleistung:

In der Regel findet eine mündliche Prüfung am Vorlesungsende statt. Bei einer sehr großen Zahl von Teilnehmern kann die Prüfung auch schriftlich erfolgen.

Lehr- und Lernmethoden:

Verwendbarkeit:

Literatur:

1. Berghammer R.: Semantik von Programmiersprachen. Logos Verlag, 2001
2. Best E.: Semantik: Theorie sequentieller und paralleler Programmierung. Vieweg Verlag, 1995
3. Loeckx J., Sieber K.: The Foundations of Program Verification. Teubner, 1984
4. Nielson H.R., Nielson F.: Semantics with Applications. A Formal Introduction. Wiley, 1992
5. Schmidt D.A.: Denotational Semantics -- A Methodology for Language Development. Allyn and Bacon, 1986
6. Winskel G.: The Formal Semantics of Programming Languages. The MIT Press, 1993

Verweise:

Kommentar:

Dieses Modul kann auch im Wahlpflichtbereich des Bachelorstudiengangs Informatik gehört werden.