Quelltext der Seite Benutzer:Stettberger/wp-Kalkül

{{DISPLAYTITLE:wp-Kalkül}}
Der '''wp-Kalkül''' ist ein [[Kalkül]] in der [[Informatik]] zur Verifikation eines [[Imperative Programmierung|imperativen Programmcodes]]. Die Abkürzung wp steht für ''weakest precondition'', auf deutsch schwächste [[Vorbedingung (Informatik)|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 (Informatik)|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 [[Assertion (Informatik)|Zusicherungen]] im Programm zu machen. Eine Zusicherung ist eine [[Prädikatenlogik|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.

<syntaxhighlight lang="cpp">
// x ist gerade
// P: (x % 2) = 0 
x = x + 1;
// x ist ungerade
// Q: (x % 2) = 1
</syntaxhighlight>

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:

# wp("", Q) = Q - Nichts passiert, die Vorbedingung bleibt gleich
# wp("[[Exception|Fehler]]", Q) = falsch - Fehler dürfen nicht auftreten
# <math>wp(A, Q) \wedge wp(A, R)  = wp(A, Q \wedge R)</math> - Distributivität der Konjunktion
# <math>wp(A, Q) \vee wp(A, R)  = wp(A, Q \vee R)</math> - Distributivität der Disjunktion

=== Sequenzregel ===
Zwei Programmstücke C<sub>1</sub> und C<sub>2</sub> können zu einem Programmstück <math>C_1 ; C_2 </math> zusammengefügt werden, wenn die Vorbedingung von C<sub>2</sub> aus der Nachbedingung von C<sub>1</sub> 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):

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

=== 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.

:<math>wp(''x := e'', Q) = Q[x/e]</math>
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:

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

=== 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.

:<math>wp(''if\ b\ then\ S_{1}\ else\ S_{2}'', Q) = [b \wedge
wp(''S_{1}'', Q)] \vee [ \neg b \wedge wp(''S_{2}'', Q)] </math>

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:

:<math>wp(''if\ b\ then\ S'', Q) = [b \wedge wp(''S'', Q)] \vee [\neg b \wedge Q]</math>

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

<syntaxhighlight lang="cpp">
// 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
</syntaxhighlight>

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:

:<math>\{ I \wedge b \} A \{ I \}</math>

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

<syntaxhighlight lang="cpp">
// { 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) }
</syntaxhighlight>

Nun gilt es nur noch folgende Schritte zu beweisen:
# Die Invariante gilt vor Schleifeneintritt
# <math>\{ I \wedge b \} A \{ I \}</math>, dass also I wirklich eine Invariante ist
# <math>(I \wedge \neg b) \Rightarrow Q</math>, dass also bei der Terminierung auch die Nachbedingung aus der Invariante folgt.
# Dass die Schleife terminiert (mittels [[Schleifenvariante]]/Terminierungsfunktion)

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

<syntaxhighlight lang="cpp">
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
</syntaxhighlight>

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

== Weblinks ==
* [http://www.logn.de/wpkalkuel/ wp-Kalkül] - Programmverifikation

== Literatur ==

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

<!-- Keine Artikelkategorien im BNR
[[Kategorie:Mathematische Logik]]
[[Kategorie:Logikkalkül]]
-->

[[bg:Предикатно-трансформативна семантика]]
[[en:Predicate transformer semantics]]
[[es:Semántica de transformación de predicados]]
[[ja:述語変換意味論]]