Benutzer:Stettberger/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.

Einleitung

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

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

Das 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 seiteneffektfrei 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

Fallunterscheidungen

Bei einer Fallunterscheidung (einem if-Statement) gibt es prinzipiell zwei mögliche Formen. Die eine, die sowohl einen then- als auch einen else-Zweig hat, und die andere die nur einen then-Zweig besitzt. Dementsprechend gibt es auch zwei Regeln diese unterschiedlichen Formen zu behandeln.

Bei der vollständigen Form mit zwei Zweigen, gilt als Vorbedingung, dass, wenn die Bedingung b zutrifft, die Vorbedingung P vor der Ausführung des then-Zweiges gelten muss. Trifft sie nicht zu, so muss sie vor dem else-Zweig gelten.

$wp(''if\ b\ then\ S_{1}\ else\ S_{2}'',Q)=[b\wedge wp(''S_{1}'',Q)]\vee [\neg b\wedge wp(''S_{2}'',Q)]$

Bei Form mit nur einem Zweig muss die Vorbedingung P vor der Ausführung des then-Zweiges gelten, wenn die Bedingung wahr ist, ansonsten, muss die Nachbedingung unverändert gelten:

$wp(''if\ b\ then\ S'',Q)=[b\wedge wp(''S'',Q)]\vee [\neg b\wedge Q]$

Ein Beispiel, an dem man sieht, dass oft mehr als das offensichtliche eine Lösung ist:

// 1. P = [ x > y AND wp("max = x", max = x)] OR [x <= y AND wp("max =y", max = x)]
// 2. P = (x > y) OR [x <= y AND wp("max = y", max = x)]
// 3. P = (x > y) OR [x <= y AND x = y]
// 4. P = (x > y) OR (x = y)
if (x > y) 
   max = x;
else
   max = y;
// Q: max = x

Mit diesen Basisregeln kann man auch die Vorbedingung zu switch-case-Konstrukten finden, indem man sie in ein if-else if-else-Konstrukt umbaut, was man wiederum als Schachtelung von if-Statements behandeln kann.

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, die ein Dazu verwendet man eine Schleifeninvariante. Sie ist ein Prädikat für das gilt:

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

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 AND b} - Invariante gilt vor dem Schleifenkörper
      A;
      // { I } - Invariante gilt nach dem Schleifenkörper
}
// { I AND (NOT 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, dass die Fakultät einer Variable x ausrechnet und in der Variable s ausgibt

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

Die Schleifenvariante ist hier (x - i). Dieser Ausdruck fällt streng monoton während der Schleifenausführung gegen 0 und ist die Abbruchbedingung.

Weblinks

• wp-Kalkül - Programmverifikation

Literatur

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