Hoare Logic. Exercise Sheet 13, Ex 6 (b)

Hello,
I wonder how to derive the precondition in Exercise 6.: Hoare Logic, b) and the solution does not help me. Am I right, that we have to use inference rules from chapter 7 here? If so, it would be really nice to see a more precise solution (the “inference tree”), because then I could figure out how exactly it works.

Yes, in this exercise, you should use the hoare calculus to prove the program correct which can also be used to derive a valid precondition (by inferring the precondition for each rule from the instantiation).

Can you share your progress on the inference tree, so we see where you are stuck?

Which rule did you try to apply first?

Did you manage to write down the tree for a?

I applied the Block rule two times, but now I am not really sure how to go on. So, I do not exactly know how to define R1, R2,…
I think that my problem is that I do not know where to start.
I did not write it down but I think i have an idea of a.The reason I started asking for b instead of a is that I think that knowing the solution of b helps me more to understand the whole topic/Exercise.

I hope that it is readable.

Unbenannt

To be precise, you have to perform the block rule once more:

...a=b*c;...   ...{b=c+a; c=c-17;}...
=====================================
...{a=b*c; b=c+a; c=c-17;}...

{b=c+a; c=c-17;} =>
b=c+a;
{c=c-17;}


{c=c-17;} => 
c=c-17;
{}

So you continue until no statement is left in the block.

Then, you resolve everything unknown as shown in the lecture from right to left.
You start with

{R3} {} {Q}

What rule applies?
What does it say about

{R2}c=c-17;{R3}

?
Do you then know any rule that applies to the resulting

{R2}c=c-17;{R3}

?
Here it will help to first understand a.
We structured the exercises such that it gets more complex from one to the other.
The solution of (a) helps you to find the solution for (b).
It is correct that if you fully understand (b), you also understand (a). But in order to understand (b), you first have to understand (a).
Therefore, it is advised to start with (a).

Okay, I went back to a) and then tried b).
I think that I understand how it works. Your feedback was already pretty helpful.

Here is what I tried:

Unbenannt

Yes, that looks good.
Only one small note:
P=R_1 is correct with the really long formula.
But P=false would require the [Consequence] rule.
Our rules (except [Consequence]) are purely syntactical.
You correctly obtained the R_i by applying the rules from right to left and substituting the assignments.
But if you want to transform the formulas into equivalent ones, you need the [Consequence] rule.

To show {false} <the whole program> {Q}, we show

false => <long R1 formula>
and 
{<long R1 formula>} <the whole program> {Q}
2 Likes

Thank you very much!