wp-Kalkül

Der wp-Kalkül ist ein Kalkül in der Informatik zur Verifikation eines imperativen Programmcodes. Die Abkürzung wp steht für weakest precondition, auf deutsch schwächste Vorbedingung. Bei der Verifikation geht es nicht darum, die Funktion mit einer bestimmten Menge an Eingabedaten auf korrekte Ergebnisse zu testen, sondern darum, eine allgemeingültige Aussage über das korrekte Ablaufen des Programms zu erhalten.

Die Überprüfung der Korrektheit geschieht durch Rückwärtsanalyse des Programmcodes. Ausgehend von der Nachbedingung wird geprüft, ob diese durch die Vorbedingung und den Programmcode garantiert wird.

Alternativ kann auch der Hoare-Kalkül benutzt werden, bei dem im Gegensatz zum wp-Kalkül eine Vorwärtsanalyse stattfindet.

Der wp-Kalkül hilft gewisse Zusicherungen im Programm zu machen. Eine Zusicherung ist eine prädikatenlogische Aussage über den Inhalt der Variablen an der bestimmten Stelle. Eine Zusicherung vor einem Programmtext heißt Vorbedingung P, eine Zusicherung danach Nachbedingung Q.

// x ist gerade
// P: (x % 2) = 0
x = x + 1;
// x ist ungerade
// Q: (x % 2) = 1

Der wp-Kalkül erlaubt es nun anhand bestimmter Regeln aus einer Nachbedingung die nötige Vorbedingung, und zwar die schwächste Vorbedingung, zu schließen, die erfüllt sein muss damit nach Ausführung des Programmcodes die Nachbedingung erfüllt ist.

Transformationen

Um die schwächste Vorbedingung P für eine Nachbedingung Q zu erhalten schreibt man P = wp(„Anweisung“, Q). Für diese Funktion gelten nun noch einige Definitionen:

1. $wp($""$,Q)=Q$ – Nichts passiert, die Vorbedingung bleibt gleich
2. $wp($„$Fehler$“$,Q)=falsch$ – Fehler dürfen nicht auftreten
3. $wp(A,Q)\wedge wp(A,R)=wp(A,Q\wedge R)$ – Distributivität der Konjunktion
4. $wp(A,Q)\vee wp(A,R)=wp(A,Q\vee R)$ – Distributivität der Disjunktion

Sequenzregel

Zwei Programmstücke C₁ und C₂ können zu einem Programmstück $C_{1};C_{2}$ zusammengefügt werden, wenn die Vorbedingung von C₂ aus der Nachbedingung von C₁ folgt.

In der konkreten Analyse eines Programms kommt man dadurch dem Ziel, einer Vorbedingung für das gesamte Programm dadurch näher, indem man die Sequenzregel anwendet und die Nachbedingung Q in eine Nachbedingung Q' überführt die eine Zeile, oder logische Einheit, weiter oben steht. Man schiebt also, bildlich gesprochen, die Zusicherung am Ende eine Zeile nach oben, indem man die Vorbedingung dieser einen Zeile ermittelt. Dazu ein kleines Beispiel (man sollte von unten nach oben lesen):

// P = wp("x = x * 2 + y", Q')
x = x * 2 + y;
// Q' = wp("x = x + 1", Q)
x = x + 1;
// Q: x < 100

Zuweisungsregel

Ist x eine Variable und e ein Ausdruck, so erhält man die schwächste Vorbedingung, indem man jedes Auftreten der Variable x in Q durch den Ausdruck e ersetzt.

$wp(''x:=e'',Q)=Q[x/e]$

Diese Ersetzung führt dazu, dass man die Auswirkungen der Zuweisungen quasi innerhalb der Nachbedingung simuliert. Diese Ersetzung kann man allerdings nur vornehmen, wenn e wirkungsfrei bezüglich Q ist, diese also nicht verändert. Dazu ein Beispiel:

// wp("x = x + 1", x > 100) = (x + 1) > 100 = x > 99
x = x + 1;
// Q: x > 100

Schleifen

Die Behandlung von Schleifen ist etwas schwieriger als die von anderen Konstrukten, da die Variablen innerhalb jedes einzelnen Schleifendurchgangs verändert werden. Daher ist es nicht einfach möglich eine starre Ersetzung vorzunehmen. Anstattdessen verwendet man eine Art Vollständige Induktion um die Funktion der Schleife nachzuweisen.

Um die schwächste Vorbedingung eines Ausdrucks der Form „while b { A }“ zu finden verwendet man eine Schleifeninvariante. Sie ist ein Prädikat für das

$\{I\wedge b\}A\{I\}$

gilt. Die Schleifeninvariante gilt also sowohl vor, während und nach der Schleife. Das Schema einer Schleife sieht dann wie folgt aus:

// { I } - Invariante gilt vor der Schleife
while ( b ) {
      // { I ∧ b} - Invariante gilt vor dem Schleifenkörper
      A;
      // { I } - Invariante gilt nach dem Schleifenkörper
}
// { I ∧ (¬b) }

Nun gilt es nur noch folgende Schritte zu beweisen:

1. Die Invariante gilt vor Schleifeneintritt
2. $\{I\wedge b\}A\{I\}$, dass also I wirklich eine Invariante ist
3. $(I\wedge \neg b)\Rightarrow Q$, dass also bei der Terminierung auch die Nachbedingung aus der Invariante folgt.
4. Dass die Schleife terminiert (mittels Schleifenvariante/Terminierungsfunktion)

Dazu ein Beispiel, das die Fakultät einer Variable x ausrechnet und in der Variable s ausgibt

i = 1;
s = 1;
// I: s = i!
while (i < x) {
      // I: s = i! ∧ i < x
      i = i + 1;
      s = s * i;
      // I: s = i!
}
// I: s = i! ∧ i >= x

Die Schleifeninvariante ist hier $(s=i!)$. Der Ausdruck $(x-i)$ fällt streng monoton während der Schleifenausführung gegen 0 und ist die Abbruchbedingung.

Literatur

• Edsger W. Dijkstra: A Discipline of Programming, Prentice-Hall, 1976.
• David Gries: The Science of Programming, Springer, 1981.