Proving the loop invariant for a simple program in Hoare logic

Question

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!

Answer 1

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$).