# Proving correctness of an iterative Fibonacci algorithm

One of the questions in the problem sets that I'm struggling in is this specific number that asks me to prove an iterative Fibonacci algorithm. The algorithm is written below:

function fib(n)
if n = 0 then
return(0)
else
a = 0; b = 1; i = 2;
while i <= n do
c = a + b
a = b
b = c
i = i + 1
return(b)


The way too prove correctness, according to my professor was to make sure that there are these three steps:

1. Initialization - the loop invariant must hold true prior to the first iteration
2. Maintenance - the loop invariant must hold true after an iteration
3. Termination - the loop invariant must hold true when the loop terminates

The loop invariant I've chosen is a <= b since I find this to be true for steps 1 through 3. First of all, I'm not sure if this is a valid loop invariant and this is the only observation I saw since i <= n isn't always true for inputs n that are natural numbers.

Assuming that I've chosen the correct loop invariant, I need to answer the proof by doing three steps so for this number I plan to answer it this way

1. Initialization - before the start of the loop a is assigned a value of 0 while b is assigned a value of 1 which starts the Fibonacci sequence. a <= b holds true prior to the start of the loop
2. Maintenance - during the loop, another variable c is added such that it is equal to the sum of a and b. After which, b is assigned to variable a while c is assigned to b thus making the invariant a <= b true during the iteration.
3. Termination - the loop ends when i > n. Before i is incremented, the procedures in the maintenance step is still done, thus the loop invariant still holds true

For my questions, is my loop invariant a <= b correct? And are the three statements I mentioned above sufficient to prove the correctness of an iterative Fibonacci algorithm?

• Although I'm not a computer scientist, I stongly suspect that your loop invariant must be related to Fibonacci numbers. Something along the lines of b being the (i-1)th Fobinacci number. Couldn't you else "prove" that your code computes anything correctly? Feb 15, 2018 at 18:31
• This is the part where I am a bit confused. Because, from what I get from the proof definition, to prove that this is correct, the loop invariant must hold true for the three cases. I am really not sure if it has something to do with correct computation. Feb 15, 2018 at 18:38
• What exactly is your question? If it is "Is a<=b a loop invariant in my algorithm?" then the answer is yes. If your question is "Does this loop invariant help me prove the algorithm correct?" then the answer is no. Feb 15, 2018 at 18:52

The condition $a \leq b$ is a loop invariant, but it captures very little of the operation of the loop. A better loop invariant is $$a = F_{i-2} \text{ and } b = F_{i-1}.$$ This clearly holds just before the loop. The loop sets $a' = b = F_{i-1}$, $b' = a+b = F_{i-2}+F_{i-1}=F_i$, $i' = i+1$, from which it is easy to prove that it maintains the loop invariant. When the loop has finished, we must have $i = n+1$, and so $a = F_{i-2} = F_{n-1}$ and $b = F_{i-1} = F_n$.
There is a weak point in this argument: How do we know that $i = n+1$ at the end of the loop? We can fix this by strengthening the loop invariant to $$a = F_{i-2} \text{ and } b = F_{i-1} \text{ and } i \leq n+1.$$ This holds just before the loop since $n \geq 1$ (assuming $n \geq 0$, a precondition that needs to be added to the entire function). It is maintained during the loop since at the beginning of each iteration $i \leq n$. Finally, after the loop we have $i \leq n+1$ and $i > n$, which forces $i = n+1$ since $i$ is an integer.