wp calculus

The wp calculus is a calculus in computer science for the verification of an imperative program code . The abbreviation wp stands for weakest precondition , in German weakest precondition . The verification is not about testing the function with a certain amount of input data for correct results, but about obtaining a general statement about the correct execution of the program.

The correctness is checked by backward analysis of the program code. Based on the postcondition, it is checked whether this is guaranteed by the precondition and the program code.

Alternatively, the Hoare calculus can be used, in which, in contrast to the wp calculus, a forward analysis takes place.

The wp calculation helps to make certain assurances in the program. An assurance is a predicate logic statement about the content of the variable at the specific point. An assurance before a program text is called precondition P, an assurance afterwards is called postcondition Q.

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

The wp calculus now allows the necessary precondition, namely the weakest precondition , to be concluded from a postcondition based on certain rules , which must be met so that the postcondition is met after execution of the program code.

Transformations

To get the weakest precondition P for a postcondition Q one writes P = wp (“instruction”, Q) . A few definitions now apply to this function:

${\ displaystyle wp (}$ "" - Nothing happens, the precondition remains the same ${\ displaystyle, Q) = Q}$
${\ displaystyle wp (}$ “ ” Errors must not occur ${\ displaystyle error}$ ${\ displaystyle, Q) = wrong}$
${\ displaystyle wp (A, Q) \ wedge wp (A, R) = wp (A, Q \ wedge R)}$ - Distributivity of the conjunction
${\ displaystyle wp (A, Q) \ vee wp (A, R) = wp (A, Q \ vee R)}$ - Distributivity of the disjunction

Sequence rule

Two program pieces C ₁ and C ₂ can be combined into one program piece if the precondition of C ₂ follows from the postcondition of C ₁ . ${\ displaystyle C_ {1}; C_ {2}}$

In the concrete analysis of a program, one comes closer to the goal of a precondition for the entire program by applying the sequence rule and converting the postcondition Q into a postcondition Q 'which is a line or logical unit above. In other words, figuratively speaking, you move the assurance one line up at the end by determining the precondition for this one line. Here is a small example (you should read from bottom to top):

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

Assignment rule

If x is a variable and e is an expression, the weakest precondition is obtained by replacing every occurrence of the variable x in Q with the expression e.

{\ displaystyle wp ('' x: = e '', Q) = Q [x / e]}

This replacement leads to the fact that the effects of the assignments are simulated within the postcondition. This replacement can only be made if e has no effect with respect to Q, i.e. it does not change it. Here is an example:

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

grind

The handling of loops is somewhat more difficult than that of other constructs because the variables are changed within each individual loop pass. Therefore it is not easy to make a rigid replacement. Instead, a kind of complete induction is used to prove the function of the loop.

A loop invariant is used to find the weakest precondition for an expression of the form “while b {A}” . She is a predicate for that

{\ displaystyle \ {I \ wedge b \} A \ {I \}}

applies. The loop invariant is valid both before, during and after the loop. The scheme of a loop then looks like this:

// { 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) }

Now there are only the following steps to prove:

The invariant applies before the loop starts
${\ displaystyle \ {I \ wedge b \} A \ {I \}}$ so that I is really an invariant
${\ displaystyle (I \ wedge \ neg b) \ Rightarrow Q}$ so that the postcondition also follows from the invariant during termination.
That the loop terminates (using the loop variant / termination function)

Here is an example that calculates the factorial of a variable x and outputs it in the variable s

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

The loop invariant is here . The expression falls strictly monotonically towards 0 during the execution of the loop and is the termination condition. ${\ displaystyle (s = i!)}$ ${\ displaystyle (xi)}$

literature

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