# Iterative Fibonacci algorithm correctness proof, finding loop invariants

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?

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.

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} \}$$1

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.