Finding a loop invariant
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)}