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.