Programmverifikation

Programmverifikation ist ein systematischer Ansatz zum Nachweis der Fehlerfreiheit von Programmen. Dabei wird bewiesen, daß ein vorgegebenes Programm bestimmte wünschenswerte Eigenschaften besitzt. Bei sequentiellen Programmen geht es vor allem um die Ablieferung korrekter Ergebnisse und die Terminierung. Bei Programmen mit parallel ablaufenden Komponenten sind zusätzliche Eigenschaften wie Interferenz-Freiheit, Deadlock-Freiheit und faires Ablaufverhalten wichtig.

In diesem Kapitel stellen wir die Grundbegriffe und Notationen zusammen, die wir im weiteren Verlauf dieses Buches voraussetzen. Wir empfehlen, jetzt zum Kapitel 3 überzugehen und von dort aus die einzelnen Abschnitte dieses Kapitels zu konsultieren. Zum Verständnis der Syntax von Programmen werden die Abschnitte 2.1 und 2.2 benötigt. Zur Behandlung der operationeilen Semantik von Programmen werden die Abschnitte 2.3 über Semantik von Ausdrücken und 2.4 über formale Beweissysteme vorausgesetzt. Für die Verifikation von Programmen, insbesondere die Definition von Korrektheitsformeln, werden die Abschnitte 2.5 – 2.7 über logische Formeln und Substitution benötigt. Die Einführung von Beweissystemen zur Programmverifikation setzt wiederum eine Kenntnis des Abschnitts 2.4 voraus. Beim Nachweis der Korrektheit der Beweissysteme wird auf das im Abschnitt 2.8 vorgestellte Substitutions-Lemma zurückgegriffen.

In einem deterministischen Programm gibt es in jedem Moment höchstens eine Anweisung, die als nächstes auszuführen ist. In Programmiersprachen wie Pascal oder Modula sind alle Programme deterministisch. In diesem Kapitel untersuchen wir eine kleine Klasse von deterministischen Programmen, die oft auch als while-Programme bezeichnet werden. Diese Klasse ist der Kern, der in allen anderen Klassen von Programmen dieses Buches enthalten ist.

In Kapitel 1 haben wir bereits gesehen, daß parallele Programme schwierig zu verstehen sein können. Deshalb werden wir sie schrittweise einführen. In diesem Kapitel betrachten wir nur die einfachste Form von Parallelismus, den sogenannten disjunkten Parallelismus. Disjunktheit bedeutet, daß die Komponenten auf gemeinsame Variablen nur Lesezugriff haben.

Disjunkter Parallelismus ist eine sehr eingeschränkte Form von Parallelismus. In Anwendungen kommt es häufig vor, daß sich parallel arbeitetende Komponenten Ressourcen wie Datenbanken, Drucker oder Datenbusse teilen. Eine gemeinsame Benutzung von Ressourcen ist notwendig, wenn es zu kostspielig ist, jede Komponente mit einer eigenen Kopie zu versorgen. Dies ist zum Beispiel bei großen Datenbanken der Fall. Eine gemeinsame Benutzung ist sogar wünschenswert, wenn dadurch Kommunikation zwischen verschiedenen Komponenten ermöglicht wird, etwa im Falle eines gemeinsamen Datenbusses. Diese Form des Parallelismus wollen wir durch parallele Programme mit Variablen modellieren, die von mehreren Komponenten gemeinsam gelesen und verändert werden können.

In den vorangegangenen Kapiteln haben wir gesehen, daß parallele Programme Nichtdeterminismus einführen, d.h. von einem festen Anfangszustand aus sind im allgemeinen mehrere Berechnungen möglich, die auch zu verschiedenen Endzuständen führen. Dieser Nichtdeterminismus ist implizit, denn wir haben bisher keine Programmkonstrukte kennengelernt, die ihn kontrollieren.