2
$\begingroup$

{Q} = {n>0}
C1 = i := 1;
C2 = c := 1;
C3 = p := 0;
{P} = {i<=n, p = fib(i-1), c = fib(i)}

My lack of understanding towards the rule of consequence in hoare logic is blocking me from find the solution which i hope someone can shed some light on how can i approach this with minimal abstraction of the process.

{R} = {i<=n,p=fib(i-1),c=fib(i)[i\1]} i:= 1;{i<=n, p = fib(i-1), c = fib(i)}

{R} = {1<=n,p=fib(0),c=fib(1)}

{R} = {1<=n,p=0,c=1}

{R1} = {1<=n,p=0,c=1[c\1]}c:=1;{1<=n,p=0,c=1}

{R1} = {1<=n, p=0, true }

{R2} = {1<=n,p=0[p\0]}p:=0;{1<=n,p=0}

{R2} = {1<=n, true}{1<=n,p=0}

{R2} = {1<=n -> 0>x} :( i can't arrive at exactly n>0

*edit

From my observation the key problem is regardless of sequence i would always arrive at 1<= n as not equivalent to n>0, i am not sure how i can legally perform P->P’ P’ C Q’ Q’->Q to prove {P}C{Q}

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

You are doing it in the opposite order. You are starting with the postcondition {i<=n, p = fib(i-1), c = fib(i)} and then computing the precondition relative to the first assignment. You should instead use the last assignment, and go backwards:

{Q} = {n>0}
{P3 = P2[i\1]} = {1<=n, 0 = fib(1-1), 1 = fib(1)}
C1 = i := 1;
{P2 = P1[c\1]} = {i<=n, 0 = fib(i-1), 1 = fib(i)}
C2 = c := 1;
{P1 = P[p\0]} = {i<=n, 0 = fib(i-1), c = fib(i)}
C3 = p := 0;
{P} = {i<=n, p = fib(i-1), c = fib(i)}

The steps above were computed bottom-up: you should read it in the same way.

It is then simple to check that Q and P3 are equivalent (assuming integer variables).

Improve this answer
$\endgroup$
4
  • $\begingroup$ What if i cannot assume integer variable and have to arrive at n>0, or is that even possible. $\endgroup$
    – Jerry Sui
    Aug 22, 2018 at 5:27
  • $\begingroup$ I can't see how the sequence of this scenario matter, as none of the assignment operation is relevant to one another so logically i would arrive at the same result regardless of the sequence. $\endgroup$
    – Jerry Sui
    Aug 22, 2018 at 6:05
  • $\begingroup$ @JerrySui You are correct in that, in this specific case, the assignments are independent so the order does not matter. Be careful, though, since usually the order does matter. Anyway, in these exercises usually one works within a programming language having only integer variables, which is what you need for your last step, i.e. rewriting 1<=n as n>0. $\endgroup$
    – chi
    Aug 22, 2018 at 7:20
  • $\begingroup$ @JerrySui More precisely, if we can choose n=0.5>0, after the three assignments, assuming the Hoare triple is valid, we would get i<=n, p = fib(i-1), c = fib(i), hence 1<=n, 0 = fib(1-1), 1 = fib(1) which is false. Hence the Hoare triple is not valid in presence of nonintegers, and by soundness, it is impossible to prove it. In the exercises I met in the past I always say integers being exploited: the step a<b iff a+1<=b is a very common one in these kinds of exercises. $\endgroup$
    – chi
    Aug 22, 2018 at 7:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.