Finding a loop invariant

Question

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 >= 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.

Answer 1

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)}