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?

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.