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 <= n}
while i < n do
{a = i + fib(i-1) /\ b = fib(i) /\ i < n}
{a = i + fib(i-1) /\ b = fib(i) /\ b − i = fib(i) - i /\ i < n}
c ← b − i
{a = i + fib(i-1) /\ b = fib(i) /\ c = fib(i) - i /\ i < n}
{a = i + fib(i-1) /\ c + a = (fib(i) - i) + (i + fib(i-1)) /\ c = fib(i) - i /\ i < n}
{a = i + fib(i-1) /\ c + a = fib(i+1) /\ c = fib(i) - i /\ i < n}
b ← c + a
{a = i + fib(i-1) /\ b = fib(i+1) /\ c = fib(i) - i /\ i < n}
{c + 2*i + 1 = fib(i) - i + 2*i + 1 /\ b = fib(i+1) /\ c = fib(i) - i /\ i < n}
{c + 2*i + 1 = fib(i) + (i+1) /\ b = fib(i+1) /\ c = fib(i) - i /\ i < n}
a ← c + 2*i + 1
{a = (i+1) + fib(i) /\ b = fib(i+1) /\ c = fib(i) - i /\ i < n}
{a = (i+1) + fib((i+1)-1) /\ b = fib(i+1) /\ (i+1)-1 < n}
i ← i + 1
{a = i + fib(i-1) /\ b = fib(i) /\ i <= n}
{a = i + fib(i-1) /\ b = fib(i) /\ i <= n /\ i >= n}
{a = i + fib(i-1) /\ b = fib(i) /\ i = n}
{b = fib(n)}