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

• Try finding the values of $a,b,c$ in terms of $i$. – Yuval Filmus May 4 '17 at 10:08

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

• Thank you, I didn't realize I can freely use the Fibonacci function like this. – Max May 4 '17 at 18:34
• You are welcome! You can do it, because the mathematical function $\mathsf{fib}$ (which is used in the purely logical part of the whole thing) is not the same thing as the fib procedure that you define in your pseudocode. We proved that fib corresponds to the ideal $\mathsf{fib}$ function. – Anton Trunov May 4 '17 at 18:47