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?