How does checking correctness with Weakest Preconditions work?

We have this example:

{true}
assume x > 1;
y := x * 2;
z := x + 2;
assert y > z;
{true}


They then show this:

{true}
wp(assume x > 1, x * 2 > x + 2) = x>1 -> x*2 > x+2
assume x > 1;
wp(y := x * 2, y > x + 2) = x * 2 > x + 2
y := x * 2;
wp(z := x + 2, y > z) = y > x + 2
z := x + 2;
wp(assert y > z, true) = y > z -> true = y > z
assert y > z;
{true}


I assume from reading other places that this is evaluated backwards, from the end to the beginning. So in steps it would be:

wp(assert y > z, true) = y > z -> true = y > z
wp(z := x + 2, y > z) = y > x + 2
wp(y := x * 2, y > x + 2) = x * 2 > x + 2
wp(assume x > 1, x * 2 > x + 2) = x>1 -> x*2 > x+2


What do the parameters mean? How do I read these statements? And how is the wp function implemented generally speaking, are there any public algorithms for it? Basically, what is happening here, can you break it down?

My reading is from this slide:

To check {P}S{Q}, prove P -> wp(S, Q)


So Q (the assertion) is the second parameter, and S (the statements) is the first parameter.

So then:

wp(assert y > z, true) = y > z -> true = y > z


We start with the Q which was {true}. We pass in the last assertion, that y > z. This for some reason results in "if y > z, then true = y > z", I don't know what that means, or how they derived this.

Then:

wp(z := x + 2, y > z) = y > x + 2


We want to prove Q = y > z. So it appears we substitute the values from S into Q, giving us y > x + 2.

Repeat this. Then we get to the end where x>1 -> x*2 > x+2, "if x > 1, then x*2 > x+2". So I still don't see how we derived this from the preceding statements.

• – D.W.
Mar 13 at 19:19
• I already looked at that page, it gives the standard derivations, but I need it spelled out like in my example, so I can see the intricacies of how it is applied. Mar 16 at 21:06