Grundlagen der Programmverifkation

Hartwig, Rolf

Teilnehmerkreis:

Studenten der Informatik und Mathematik im Hauptstudium, die sich für Fragen der Theoretischen Informatik interessieren

Übersicht:

Die Computerprogrammierung ist eine "exakte Wissenschaft" in dem Sinne, daß alle Eigenschaften eines Programms prinzipiell rein deduktiv aus dem Programmtext abgeleitet werden können. Im Widerspruch dazu steht allerdings die Praxis des Experimentierens mit "fertigen" Programmen ("Testphase"), um diese fehlerfrei (?) zu machen.
Notwendig sind exakte Methoden der Programmdokumentation und Programmverifikation. Notwendig ist eine Programmiermethodologie, die sich auf Beweise - nicht auf das Testen - von Programmeigenschaften stützt.

Die Vorlesung führt in dazugehörige mathematische Grundlagen ein und stellt den Anschluß an die Literatur auf diesem Gebiet her.

Wesentliche Stichworte zum Inhalt der Vorlesung sind:
Korrektheit von Programmen, Axiomatische Semantik, HOARE-Logik, asserted programs, Prädikattransformer, COOK-Vollständigkeit.

Gliederung:

1. Einleitung:
   allgemeiner Kalkülbegriff, grundlegende Begriffe und Bezeichnungen
2. Formale Theorien für Programmiersprachen:
   Programmspezifikationen und Beweissysteme
   Beispiele
3. HOARE-Logik für while-Programme:
   Geradeausprogramme
   Vorbedingung, Nachbedingung, Ausdrucksfähigkeit
   FLOYDsches Vorwärts-Zuweisungsaxiom
   Behandlung der Iteration
4. Ausblick: Indizierte Variablen, Blockstruktur

Literatur:

• de Bakker, J.W. Mathematical Theory of Program Correctness. 1980, Prentice Hall Int., Englewood Cliffs
• Futschek, G. Programmentwicklung und Verifikation. 1989, Springer-Verlag
• Gries, D. The Science of Programming. 1981, Springer-Verlag
• Kowalk, Wolfgang P. Korrekte Software. Semantik, Spezifikation, Verifikation und Testen von Programmen. 1993, BI-Wissenschaftsverlag
• Loeckx, J. and Sieber, K. The Foundation of Program Verification. 1987, Teubner Stuttgart
• Riedewald, G. u.a. Formale Beschreibung von Programmiersprachen. 1983, Akademie-Verlag Berlin

Erwartete Vorkenntnisse:

Kenntnis einer höheren Programmiersprache
Grundkenntnisse der mathematischen Logik

Scheinvergabe:

Bei regelmäßigem Vorlesungsbesuch

Sonstiges:

Zur Vorlesung gibt es ein gut ausgearbeitetes Skript.