Finding a loop invariant the following pseudo code returns the nth Fibonacci number:

 if n = 0 then
    return 0
 a ← 1
 b ← 1
 for i = 1 to n − 1 do
     c ← b − i
     b ← c + a
     a ← c + 2*i + 1
 return b


I am trying to find any loop invariant for the variables a and b, (as i understand it has to be valid before and after the loop, but i can't seem to be able to come up with anything, except maybe b &gt;= i, but I'm not sure that counts as an invariant). As far as I get it, simply saying b = b - i + a wouldn't really mean anything. Any help on the subject would be greatly appreciated.
As we already know, the loop iteratively calculates the nth Fibonacci number, so it naturally follows that the loop invariant should contain $b = \mathsf{fib}(i)$ condition.
But that is not sufficient for us, because the computation depends on the variable a, and we don't need c, because it is initialized in the loop body.

The line b ← c + a actually gives us a hint as to what the condition on a should we impose: after this line $b$ must be equal to $\mathsf{fib}(i+1)$. Now, from the expression for c and the expression $\mathsf{fib}(i+1) = \mathsf{fib}(i) + \mathsf{fib}(i-1)$ we easily obtain the condition for a: $a = \mathsf{i + fib(i-1)}$.

If we rewrite the for loop into an equivalent while loop, we'll get a loop invariant:

$$a = i + \mathsf{fib}(i-1) \wedge b = \mathsf{fib}(i) \wedge i \le n.$$

Here is how we can prove that the loop actually does the job:

{a = i + fib(i-1) /\ b = fib(i) /\ i &lt;= n}
while i &lt; n do
  {a = i + fib(i-1) /\ b = fib(i) /\ i &lt; n}
  {a = i + fib(i-1) /\ b = fib(i) /\ b − i = fib(i) - i /\ i &lt; n}
  c ← b − i
  {a = i + fib(i-1) /\ b = fib(i) /\ c = fib(i) - i /\ i &lt; n}
  {a = i + fib(i-1) /\ c + a = (fib(i) - i) + (i + fib(i-1)) /\ c = fib(i) - i /\ i &lt; n}
  {a = i + fib(i-1) /\ c + a = fib(i+1) /\ c = fib(i) - i /\ i &lt; n}
  b ← c + a
  {a = i + fib(i-1) /\ b = fib(i+1) /\ c = fib(i) - i /\ i &lt; n}
  {c + 2*i + 1 = fib(i) - i + 2*i + 1 /\ b = fib(i+1) /\ c = fib(i) - i /\ i &lt; n}
  {c + 2*i + 1 = fib(i) + (i+1) /\ b = fib(i+1) /\ c = fib(i) - i /\ i &lt; n}
  a ← c + 2*i + 1
  {a = (i+1) + fib(i) /\ b = fib(i+1) /\ c = fib(i) - i /\ i &lt; n}
  {a = (i+1) + fib((i+1)-1) /\ b = fib(i+1) /\ (i+1)-1 &lt; n}
  i ← i + 1
  {a = i + fib(i-1) /\ b = fib(i) /\ i &lt;= n}
{a = i + fib(i-1) /\ b = fib(i) /\ i &lt;= n /\ i &gt;= n}
{a = i + fib(i-1) /\ b = fib(i) /\ i = n}
{b = fib(n)}