2
$\begingroup$
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?

$\endgroup$
  • 1
    $\begingroup$ $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. $\endgroup$ – user21820 Aug 11 '15 at 11:46
  • 1
    $\begingroup$ Well I want to prove that the algorithm is correct $\endgroup$ – hasyren Aug 11 '15 at 11:47
  • $\begingroup$ What is the meaning of correct? $\endgroup$ – user21820 Aug 11 '15 at 11:49
  • 1
    $\begingroup$ 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. $\endgroup$ – user21820 Aug 11 '15 at 11:51
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Use LaTex , MathJax $\endgroup$ – 3SAT Aug 11 '15 at 11:57
  • $\begingroup$ I used LaTex for your answer. Please check that I did not alter anything. $\endgroup$ – Claude Leibovici Aug 11 '15 at 12:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.