# loop invariant fibonacci

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?

• $1 = 1$ is a loop invariant. The point is that you have not specified at all what you want to prove, so there is no goal and hence no need for any particular loop invariant. – user21820 Aug 11 '15 at 11:46
• Well I want to prove that the algorithm is correct – hasyren Aug 11 '15 at 11:47
• What is the meaning of correct? – user21820 Aug 11 '15 at 11:49
• Note that the one who posted an answer had to guess what you wanted to prove. Yes you wrote "fibonacci" in the title but so what? To make things clear you would have to define what the correct output should be. – user21820 Aug 11 '15 at 11:51

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.