Vorlesungsankündigung
(Sommersemester 1999)
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.
Termin: Dienstag 12-14 Uhr, V 301
Übung:
Mittwoch 10-12 Uhr, V 34