WP Calculator

Calculation of the weakest precondition of a simple program fragment

WPCalc

In class, computer science students learn to use the program verification method to determine the weakest precondition given a program and specification. Even the smallest program fragments give rise to long logical expressions whose simplification is time-consuming and highly error-prone.

WPCalc is able to simplify logical expressions and to determine the weakest precondition WP from a program fragment P in pseudo-code with given postcondition S. Furthermore, given precondition R, the implication R->WP can be checked.

WPCalc is a Java console program and the output is generated either in tree or linear form.

Program Example

Pre: ((x >= 0) && (x <= 2147483647))
a := x;
b := y;
r := 0;
while (a != 0) do
   if ((a & 1) = 1) then
      r := (r + b);
   end
   b := (b << 1);
   a := (a >> 1);
end
Post: (r = (x*y))
  • precondition R of program P: R is (x >= 0) && (x <= 2147483647)
  • postcondition S of program P: S is r = (x*y)
  • weakest precondition WP = wp(P, S)
  • simplified weakest precondition WP is (x >= 0)
  • implication to prove: R -> WP is true

WPCalc Linear Output

WP before simplification has length of 250 characters
[250] (((!(x != 0) || ((((x & 1) = 1) && (((x >> 1) >= 0) && ((((x >> 1)(y <> 1) >= 0) && ((((x >> 1)(y <= 0) && (((xy) + 0) = (xy)))) 
[196] ((((((([x/2] >= 0) && ((([x/2](y2)) + y) = (xy))) && ((x%2) = 1)) || ((([x/2] >= 0) && (([x/2](y2)) = (xy))) && ((x%2) != 1))) || (x = 0)) && (((x = 0) || (x != 0)) || (y = 0))) && (x >= 0)) 
[163] (((((((x - 1) >= 0) && (((1(y(x - 1))) + y) = (xy))) && ((x%2) = 1)) || ((((x - 0) >= 0) && ((1(y(x - 0))) = (xy))) && ((x%2) = 0))) || (x = 0)) && (x >= 0)) 
[116] ((((((x >= 1) && (((1 + (x - 1))y) = (xy))) && ((x%2) = 1)) || ((x >= 0) && ((x%2) = 0))) || (x = 0)) && (x >= 0)) 
[110] ((((((x >= 1) && (((0 + x)y) = (x*y))) && ((x%2) = 1)) || ((x >= 0) && ((x%2) = 0))) || (x = 0)) && (x >= 0))
[ 69] ((((x >= 0) && (((x%2) = 1) || ((x%2) = 0))) || (x = 0)) && (x >= 0))
[  8] (x >= 0)
To prove: (!((x >= 0) && (x = 0))
Simplified implication: true

Contact

Prof. Dr. Christoph Stamm

Dozent für Informatik

Telefon: +41 56 202 78 32(Direkt)
E-Mail: christoph.stamm@fhnw.ch
×