Proving correctness of an iterative Fibonacci algorithm

Question

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?

• tobwin: 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?
• Jessie: 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.
• tobwin: 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.

Answer 1

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.

• Jessie: Now I see the part where the computation of the Fibonacci takes place. I was thinking of something like this but I just couldn't properly sew it in. I guess the part of determining the loop invariant is the most important part for proving iterative algorithms