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:

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.