loop invariant fibonacci

Question

fibonacci(int n)
if n < 0
return 0;

else if n = 0
return 0;

else if n = 1
return 1;

else x = 1;
y = 0;
for i from 2 to n {
    t = x;
    x = x + y;
    y = t;
}

}
return x;

I'm trying to find a loop invariant for the above algorithm, but am not sure where to start. I know that the invariant must hold true immediately before and after completion of the loop. How would I go about doing this?

Answer 1

Let $f(n)$ be the $n^{th}$ term of the Fibonacci sequence.

A correct invariant would be, for example: " At the end of an iteration , $y=f(i-1)$ and $x=f(i)$ " It is true for the first iteration ($i=2, y=1, x=1$), and stays true during the loop due to the definition of $f$ ($f(n)=f(n-1)+f(n-2)$ for $n > 1$).

Hence, at the end of the loop, $x=f(i)=f(n)$, so the function returns the correct value.