Proving the loop invariant for a simple program in Hoare logic
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&lt;10$, implies $i=10$ (the $j=-1$ part then follows from $i+j=9$).