Exercise sheet 14 9b

Hi,
I got a little problem understanding the solution of this exercise.
After using Consequence, the precondition is still {I and (b>0)}, but after using [Block] then the (b>0) just randomly (to me) disappears. I got exactly the same solution doing the exercise, but I wonder how I can just omit parts of the precondition, shouldn’t it be changed after using [Consequence]?

1 Like

How did you arrive at this solution? In which order and why did you apply the rules?
What do you have to check for each step?

well at first I went “up” until I was able to use [BLock0] on the top right and then I went left using the precondition I got from there as a postcondition for the next thing and so on.

then it was basically just using [Assign]

For just going, you can directly apply the Block rule (without Consequence). Did you do this? Why or why not (what problems arise)?

I did not because my tutor told me to always use Consequence at first but I don’t really get why in this case

Try to draw the tree without consequence.
Just Block, Assign, Block0. Apply the rules exactly (write down the instantiations you used for P, Q, R, s, c, …). What do you notice?

sorry I really don’t get it, there is the exact same thing in the tree before and after using Consequence, so I guess there should be the same outcome?

For now, do not look at the solution. They contain a typo/mistake.
We first want to solve the exercise to see why we need the [Consequence] rule in general and for invariants in particular.
You will notice the problem of the solution when writing down the rule instantiations (P, Q, R).

yes that’s exactly my problem.
in the second layer (from below) is the precondition {I and b>0} and in the third it is just {I}
That was why I was asking

Yes, the [Consequence] rule would allow to drop the \land b>0 from the precondition (which was added by the while loop).
You would add the proof and write in the second to last line I.
Does the proof go through with this change?

I don’t see why it should not.

What are your (precondition, postcondition) instantiations for the [Consequence] and first (that is bottom-most) [Block] rule?

well just P={I and b>0} and Q ={I} what I got from the [While] rule or am I wrong?

Tha is the goal you want to prove.
Then you apply the rules.
From what I understand you are doing, you first apply [Consequence]
instantiated with:

Q'=Q=I
s = {x=x+a;b=b-1;}
P' = I && b>0
P = I

Screenshot_20220726_122616

You are left to prove {I} s {I}.
Screenshot_20220726_122817

Now you apply [Block] with

P = I
Q = I
s1 = (x=x+a)
..., sn = (b=b-1)
R = (x=(B-(b-1))*a)

These would be the instantiations you get directly and after applying Block, Block0, Assign (for R).

You are left to prove (on the left side):

{P} s1 {R}

{I} x=x+a; {x=(B-(b-1))*a}

I = (x=(B-b)*a)
{x=(B-b)*a} x=x+a; {x=(B-(b-1))*a}

as stated in the block rule.

What rule do you apply (with which instantiations)?

exactly.

I tried applying Assign with Q = {x = (B-(b-1))*a} and got P = {x = (B-b)*a} = I

Screenshot_20220726_123633

Assign with Q=(x=(B-(b-1))*a) and e=x+a is:

|- {x+a=(B-(b-1))*a} x=x+a; {x=(B-(b-1))*a}

But
x+a=(B-(b-1))*a is not (syntactically) x=(B-b)*a.

Therefore, you can not apply [Assign].

But can’t I just subtract a on both sides?

Yes, both formulas are equivalent (if one holds, the other holds).
But they are not the same.
As I tried to emphasize with the substitutions, our Hoare calculus is a set of syntactical rules.
You match and apply with exact matches.
The only semantical rule (which requires creativity and generates conditions for pc and vc) is [Consequence].
[Consequence] allows to strengthen and weaken pre- and post-conditions (semantically).
That is, you have to use [Consequence] if you want to transform something.

okay, so the correct solution would be transforming the Precondition from {I and b>0} to {x+a = (B-(b-))*a} in the second layer?