Vorlesungsankündigung

(Sommersemester 2001)

Prof. Dr. Helmut Seidl:

Formale Semantik

Prof. Dr. Helmut Seidl - Übersetzerbau - Informatik
Programme einer Programmiersprache sollten eine wohldefinierte ``Bedeutung'' haben. Sicherlich könnte man sich darauf beschränken zu sagen: ``die Bedeutung ist, was der Compiler (und dann die Programmausführung) mit dem Programmtext anstellt''. Da die Programmiererin i.a. den Compiler nicht selbst geschrieben hat und ihn darum nicht wie ihre Westentasche kennt, hat dieses Vorgehen den Nachteil, daß die Programmiererin - oder später die Anwenderin - des öfteren böse Überraschungen erleben wird. Es erscheint darum nur sinnvoll, die Semantik von Programmen einer Programmiersprache direkt, d.h. unabhängig von möglichen Compilern zu spezifizieren. Ein solches Vorgehen ermöglicht nicht nur, formal nachzuvollziehen, warum das Programm nicht tut, was es tun soll, sondern eventuell zu beweisen, daß es sich stets richtig verhält. Die Vorlesung stellt einige Methoden vor, wie die Bedeutung eines Programms formal angegeben werden kann bzw. wie Zusicherungen über das Programm formal bewiesen werden können. Als Beispiel einer ``ausführbaren'' Semantik werden wir dabei eine funktionale Programmiersprache kennenlernen.

Termine:

Vorlesung: Montag 10-12 Uhr, V 301

Übung: Freitag 12-13 Uhr, V 301

Scripte zur Vorlesung: