2
$\begingroup$

I was studying loop invariant and came across Tomas Petricek's example. Here's the equivalent(I believe) program after I revised it a bit for proof in Hoare logic:

j = 9;
i = 0;
while (i < 10)
{
    i = i + 1;
    j = j - 1;
}

The loop invariant given by Petricek is i + j == 9, which makes sense to me. And the pre-condition and post-condition, seems to me, is (|T|) and (|i = 10 and j = -1|), respectively. Here's my attempt:

(| T |) 
(| eta[j/9][i/0] |) Implied
  i = 0;
(| eta[j/9] |) Assignment
  j = 9;
(| eta |) Assignment
  while (i < 10)
  {
    (| eta and i < 10|)
    (| eta[j/j-1][i/i+1] |) Implied
      i = i + 1;
    (| eta[j/j-1] |) Assignment
      j = j - 1;
    (| eta |) Assignment
  }
(| eta and not i < 10 |) While
(| i = 10 and j = -1 |) Implied

For the three Implied rule, with eta being i + j = 9, the first two are straightforward to me:

|- T => 0 + 9 = 9
|- i + j = 9 and i < 10 => i+1 + j-1 = 9

But I can't see how do I get from i + j = 9 and not i < 10 to i = 10 and j = -1. Am I setting the wrong post-condition? I could get j <= -1 trivially, but I don't think that's how it should work, right?

I thought that, without setting j to 9 and i to 0 in first two line, what this while loop does is to set i to 10 and j to j-(10-i). In that case, if we set the initially value of i to 0 and j to 9, j would be set to 9-(10-0) = -1, which is what I intended. I'm not sure what went wrong in my reasoning. May I have a hint? Thanks!

$\endgroup$
4
$\begingroup$

Your invariant, together with the negation of the loop condition, is not strong enough to imply your postcondition. Try adding an additional conjunct to the invariant which, together with $\neg\ i<10$, implies $i=10$ (the $j=-1$ part then follows from $i+j=9$).

$\endgroup$
  • $\begingroup$ I was thinking about making invariant i + j = 9 and i < 11 which works for post condition. But does that mean i + j = 9 is not a good invariant or is my intended post condition not chosen correctly?(the original answer didn't mention pre/post) so I made up i=10 and j=-1 which seems right $\endgroup$ – RexYuan Mar 17 '17 at 13:38
  • 1
    $\begingroup$ @RexYuan Your post-condition is correct (you were able to prove it, after all). Your original invariant is also correct, just not strong enough to prove the post-condition; adding $i<11$ results in another invariant which is correct and strong enough, as you found out. There is usually a balancing act: the invariant should be (i) inductive, (ii) strong enough to imply the intended post-condition, and (iii) weak enough to follow from the pre-condition. As such, the notion of any given invariant being inherently "good" or "bad" is a bit tricky. $\endgroup$ – Klaus Draeger Mar 17 '17 at 14:52

Your Answer

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

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