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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top