1
$\begingroup$

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.

$\endgroup$
2

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.