wp-Kalkül – Programmverifikation

Beim Entwickeln von Programmen ist es wahrscheinlich, dass Fehler gemacht werden, und das Programm am Ende nicht immer korrekt abläuft. Es gibt verschiedene Methoden, wie man versuchen kann die Korrektheit eines Programms zu verifizieren.

Die trivialste Möglichkeit ist das Testen mit einer bestimmten Menge von Eingabedaten. Liefert das Programm immer das erwartete Ergebnis, so weiß man, dass für die getesteten Eingabedaten das Programm korrekt abläuft. Man hat jedoch keine allgemeine Aussage über die Korrektheit des Programms.

In diesem Artikel wird auf eine mathematische Möglichkeit eingegangen, wie man beweisen kann, dass ein Programm korrekt ist, und zwar über den wp-Kalkül. Der Artikel wird etwas länger werden, da das Thema nicht so ganz einfach ist, und ich lieber etwas ausführlicher die Sachen herleite.

Zusicherungen (Assertions)

Der wp-Kalkül untersucht die Korrektheit von imperativen Programmen. Wir möchten also gewisse Zusicherungen an unser Programm an bestimmten Stellen im Code machen können. Eine Zusicherung ist ein prädikatenlogischer Ausdruck über die Belegung von Programmvariablen an der Stelle vom Programm, an der die Zusicherung erfolgen soll.

Eine Zusicherung vor dem zu untersuchenden Programmteil nennen wir Vorbedingung $Q$ und eine Zusicherung nach dem Programmteil Nachbedingung $P$ .

Ein kleines Beispiel könnte so aussehen:

// Vorbedingung P: y > 1
x := y^2;
// Nachbedingung Q: x > y > 1

Wenn also die Vorbedingung $y > 1$ gilt, so gilt natürlich auch die Nachbedingung $x > y > 1$ , wenn wir das (kurze) Programm durchlaufen haben.

Verifikation und Korrektheit

Eine Verifikation prüft nun ob das Programm bestimmte Zusicherungen erfüllt. Wenn wir also eine Anweisungsfolge $A$ haben, und eine Vorbedingung $P$ , möchten wir verifizieren können, dass nach Abarbeitung von $A$ mit Vorbedingung $P$ , die Nachbedingung $Q$ folgt.

Wir definieren uns hierfür zwei Arten der Korrektheit:

1. Partielle Korrektheit

Wenn die Ausführung von $A$ in einem Zustand, der $P$ genügt, beginnt und falls die Ausführung von $A$ nach endlich vielen Schritten terminiert, dann erfüllt der erreichte Zustand $Q$ .
Schreibweise: $P \{A\} Q$

2. Totale Korrektheit

Siehe (1). Verlangt zusätzlich den Beweis der Terminierung.
Schreibweise: $\{P\} A \{Q\}$

Unsere (imperativen) Programme bestehen nicht nur aus einzelnen Anweisungen, sondern aus linearen Strukturen (z.B. Folgen von Anweisungen, Schleifen, …). Dies bedeutet wiederum, dass man aus der Korrektheit einzelner Teile des Programms die korrektheit des gesamten Programms beweisen kann.

Der wp-Kalkül beruht hierbei auf der Rückwärtsanalyse. Man stellt sich also die Frage: Welche Vorbedingung $P$ muss mindestens erfüllt sein, damit nach dem Ablauf des Programms eine gegebene Nachbedingung $Q$ vorliegt? Das „mindestens“ ist sehr wichtig, denn es gibt für die eine Nachbedingung $Q$ mehrere Vorbedingungen $P$ von denen uns aber nur die schwächste (weakest precondition) interessiert, daher auch der Name des Kalküls.

Definitionen und Regeln

Der wp-Kalkül ist wie folgt definiert:

Wenn $Q$ ein Prädikat ist und $A$ eine Anweisungsfolge ist, dann ist die schwächste Vorbedingung von $A$ in Bezug auf $Q$ , $\text{wp}(A,Q)$ , ein Prädikat, das die Menge aller Startzustände beschreibt, so dass wenn die Ausführung von $A$ in einem der Zustände beginnt, die Ausführung in einem Zustand, der $Q$ genügt, terminiert.

Schreibweise: $\text{wp}(\texttt{anweisungen}, Q) = P$ .
$P$ ist schwächste Vorbedingung.

Zusätzlich seien noch folgende Definitionen gegeben:

$\text{wp}(\texttt{leer}, Q) = Q$
“Wenn nichts passiert ändern sich die Bedingungen nicht.”

$\text{wp}(\texttt{fehler}, Q) = \texttt{false}$
“Fehler dürfen nicht passieren.”

$\text{wp}(\texttt{abbruch}, Q) = \texttt{false}$
“Nach Abbruch gilt nichts mehr.”

Daraus lassen sich die folgenden Rechenregeln ableiten ( $A$ bzw $B$ seien hierbei beliebige Anweisungsfolgen):

$\text{wp}(A, \texttt{false}) = \texttt{false}$
Ausgeschlossene Wunder.

$\text{wp}(A, Q) \land \text{wp}(A, R) = \text{wp}(A, Q \land R)$
Distributivität der Konjunktionen.

$\text{wp}(A, Q) \lor \text{wp}(A, R) \Rightarrow \text{wp}(A, Q \lor R)$
Distributivität der Disjunktionen.

Wenn $Q \Rightarrow R$ dann $\text{wp}(A, Q) \Rightarrow \text{wp}(A, R)$
Monotonie.

$\text{wp}(\texttt{"$A$; $B$;"}, R) = \text{wp}(\texttt{"$A$;"}, \text{wp}(\texttt{"$B$;"}, R))$
Seuqenzregel.

Wenn $Q \Rightarrow Q'$ gilt:
$\{P\} A \{Q\} \land \{Q'\} B \{R\} \Rightarrow \{P\} A; B; \{R\}$
Erweiterte Sequenzregel.

$\text{wp}(\texttt{"x := e"}, Q) = Q\ [x/e]$ , wobei $x$ eine Variable und $e$ ein Ausdruck
Zuweisungsregel.

$\text{wp}(\texttt{"if $B$ then $S_1$ else $S_2$"}, Q) = (B \Rightarrow \text{wp}(S_1, Q)) \lor (\neg B \Rightarrow \text{wp}(S_2, Q))$ wenn $B$ seiteneffektfrei
Fallunterscheidung (If-Then-Else-Regel).

$\text{wp}(\texttt{"if $B$ then $A$"}, Q) = (B \Rightarrow \text{wp}(A, Q)) \lor (\neg B \Rightarrow Q)$
Fallunterscheidung (If-Then-Regel ohne Else-Teil).

Schleifen

Schleifen sind etwas komplizierter zu verifizieren, da hier ein Programmabschnitt $S$ so oft wiederholt wird (potentiell unendlich oft), bis eine Schleifenbedingung $B$ nicht mehr erfüllt ist. Man beachte, dass man jede Art von Schleife auf die while-Schleife zurückführen kann, so dass wir im wp-Kalkül nur while-Schleifen betrachten.

Man könnte eine Schleife als geschachtelte Form von if-then-else Anweisungen betrachten, in etwa dieser Form:

wp("while B do S") =
         ¬B ⇒ Q ∧
              B ⇒ wp(S, ¬B ∧ Q ∧
                  B ⇒ wp(S, ¬B ⇒ Q ∧
                       B ⇒ wp(S, …)))

Dies ist absolut unhandlich und praktisch nicht zu lösen, daher gibt es einen anderen Lösungsweg.

Hierfür sucht man sich (durch „raten“) als erstes eine Schleifeninvariante $I$ . Dies ist eine Zusicherung, die vor, während und nach der Schleife gelten muss. Wichtig ist, dass dieser Ausdruck möglichst stark ist, und eine Aussage über den Bereich der Laufvariable, sowie den jeweils aktuellen Wert der zu berechnenden Variable in Abhängigkeit von der Laufvariablen enthält!

Das Schema einer Schleife sieht demnach folgendermaßen aus ( $S$ ist die Anweisungsfolge im Schleifenrumpf):

{I}
while B do
    {I ∧ B} S {I}
{I ∧ ¬B}
{Q}

Hat man seine Invariante gefunden, kann man nun nach folgendem Rezept vorgehen um die Schleife zu verifizieren:

Zeige dass $I$ vor der Schleife gilt. (nicht via wp-Kalkül)
Beweise über wp-Kalkül: $\{I \land B\} S \{I\}$
Zeige: $\{I \land \neg B\} \Rightarrow Q$
Zeige dass Schleife terminiert.

www log₂(n) de