# Proving the loop invariant for a simple program in Hoare logic

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!

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$).
• @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. Mar 17 '17 at 14:52