Wp-Kalkül - LinkFang.de





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. [math]wp(A, Q) \wedge wp(A, R) = wp(A, Q \wedge R)[/math] – Distributivität der Konjunktion
  4. [math]wp(A, Q) \vee wp(A, R) = wp(A, Q \vee R)[/math] – Distributivität der Disjunktion

Sequenzregel

Zwei Programmstücke C1 und C2 können zu einem Programmstück [math]C_1 ; C_2 [/math] zusammengefügt werden, wenn die Vorbedingung von C2 aus der Nachbedingung von C1 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.

[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:

// 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

[math]\{ I \wedge b \} A \{ I \}[/math]

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 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. [math]\{ I \wedge b \} A \{ I \}[/math], dass also I wirklich eine Invariante ist
  3. [math](I \wedge \neg b) \Rightarrow Q[/math], 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 + 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 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.

Kategorien: Keine Kategorien vorhanden!

Quelle: Wikipedia - http://de.wikipedia.org/wiki/Wp-Kalkül (Vollständige Liste der Autoren des Textes [Versionsgeschichte])    Lizenz: CC-by-sa-3.0

Änderungen: Alle Bilder mit den meisten Bildunterschriften wurden entfernt. Ebenso alle zu nicht-existierenden Artikeln/Kategorien gehenden internen Wikipedia-Links (Bsp. Portal-Links, Redlinks, Bearbeiten-Links). Entfernung von Navigationsframes, Geo & Normdaten, Mediadateien, gesprochene Versionen, z.T. ID&Class-Namen, Style von Div-Containern, Metadaten, Vorlagen, wie lesenwerte Artikel. Ansonsten sind keine Inhaltsänderungen vorgenommen worden. Weiterhin kann es durch die maschinelle Bearbeitung des Inhalts zu Fehlern gerade in der Darstellung kommen. Darum würden wir jeden Besucher unserer Seite darum bitten uns diese Fehler über den Support mittels einer Nachricht mit Link zu melden. Vielen Dank!

Stand der Informationen: August 201& - Wichtiger Hinweis: Da die Inhalte maschinell von Wikipedia übernommen wurden, ist eine manuelle Überprüfung nicht möglich. Somit garantiert LinkFang.de nicht die Richtigkeit und Aktualität der übernommenen Inhalte. Sollten die Informationen mittlerweile fehlerhaft sein, bitten wir Sie darum uns per Support oder E-Mail zu kontaktieren. Wir werden uns dann innerhalb von spätestens 10 Tagen um Ihr Anliegen kümmern. Auch ohne Anliegen erfolgt mindestens alle drei Monate ein Update der gesamten Inhalte.