Iterative Fibonacci algorithm correctness proof, finding loop invariants

Question

The algorithm take in an integer $n$ and outputs the $n$th number in the Fibonacci sequence ($F_n$). The sequence starts with $F_0$. I am trying to prove the correctness assuming valid input:

int Fib(int n) {
    int i = 0;
    int j = 1;
    int k = 1;
    int m = n;
    while(m >= 3){
        m = m-3;
        i = j +k;
        j = i+k;
        k = i + j;
    }
    if(m == 0 ){
        return i;
    }
    else{
        if(m == 1){
            return j;
        }
        else{
            return k;
        }
    }
}

For a reminder, a loop invariant is a claim which holds every time just before the loop condition is checked. It holds even when the loop condition is false. I've established and proven one loop invariant that $m \geq 0$. This helps me show that the algorithm terminates since when the loop exits since $m$ is either 0, 1, or 2. However, I'm stuck on finding another loop invariant that would help me show that the algorithm produces the correct Fibonacci number.

One pattern I found is that the result of returning i, j, or k is due to the result of the initial value of $m$ $\% 3$. Depending on the remainder, either i, j, or k is returned. I tried expanding this idea further but led myself to a dead end. I'm thinking I need to find some way to express $F_n = F_{n-1} + F_{n-2}$ in terms of i, j and k in order to prove that the program outputs correctly. Am I on the right track with remainders or is there something I'm missing?

Answer 1

Assume n=0, n=1 or n=2. For your program to be correct, you need i = Fib(0), j = Fib(1) and k = Fib(2). Now assume 3 ≤ n < 6. For your program to be correct, you need i = Fib(3), j = Fib(4) and k = Fib(5) after the first iteration. Check that.

Let d = n-m. Then before the first iteration, d = 0 and after the first iteration, d = 3. With what I wrote above I think you need i = Fib(d), j = Fib(d+1), k = Fib(d+2) before each iteration. Now all you need is put everything together.

Of course you could compile the code, use a debugger, and check which values are actually calculated let's say if n = 10 (or do it by hand). It would help a lot if you actually understood what the program does.

Answer 2

It kind of depends on what formalism you want to use for this proof.. But the core-idea which holds for pretty much any such formalism is the following:

Suppose you establish some invariant $I$ you will want to be able to make the following conclusion

$$ m < 3 \land I \implies X $$

where $X$ tells you that the values $i,j$ and $k$ have the right values.

You are on the right track with the argument $I = I' \cup \{ m = n \mod 3 \}$, however $I' = \{m \geq 0\}$ is way too weak to establish that $\texttt{Fib}(n)$ returns the $n$th Fibonacci number.

---

Try the following:

• Find some existential (for some value, eg. $z$) claim about the relationship of $n$ and $m$ (seems like you already did so)
• Now use that value $z$ to show $\{ k = F_z, i = F_{z-2}, j = F_{z-1} \}$¹

I hope this will help you!

_{1: Depends on your claim about $m$ and $n$, could also be shifted $\{ k = F_{z+2}, i = F_z, j = F_{z+1} \}$ as in gnasher729's answer which is simpler. The core idea is the same.}