Prove correctness for computing the nth Fibonacci number for the pseudo code

Question

How do we prove the correctness of this pseudo code by induction?

fastfib(integer n)
if n < 0 return 0;
else if n = 0 return 0;
else if n = 1 return 1;
else a ← 1; b ← 0;
   for i from 2 to n do
       t ← a; a ← a + b; b ← t;
return a;
end

Answer 1

The idea is that at the end of the $i$th iteration, $a = F_i$ and $b = F_{i-1}$. This is something that you can easily prove by induction. (Usually this sort of condition is called a loop invariant.)

Answer 2

Try to

• simplify the program and
• get it into a more functional form.

So

• Dump the negative case - there is no -3rd Fibonacci number.
• You can do without the explicit $1 \mapsto 1 $. No times round the loop gives that result.
• The function applied round the loop is $[a, b] \mapsto [a+b, a]$.
• If you take $b$ instead of $a$, you can get rid of the $0 \mapsto 0$ case too.

You then have something you can reason inductively about.

---

I find it much more convincing with real than with pseudo code. Translating your pseudo-code into Clojure ...

(defn fast-fib [n]
  (case n
    0 0
    1 1
    (first
      (nth (iterate
             (fn [[a b]]
               (let [t a
                     a (+ a b)
                     b t]
                 [a b]))
             [1 0])
           (- n 1)))))

... which the above transformations turn into the equivalent ...

(defn fast-fib [n]
    (second
      (nth (iterate
             (fn [[a b]] [(+ a b) a])
             [1 0])
           n)))

... which is much easier to reason about.

Other functionally expressive programming languages are available.

Answer 3

Here's my approach:

First I check that the code is indeed possibly correct by checking that it gives the correct result for say all n ≤ 10. If not then you have your answer.

Second I determine the values of a and b for 2 ≤ i ≤ 10 and see if I can find a pattern. If I can't find a pattern then I ask for help. If I find a pattern, then I use induction to prove the following:

If n ≥ 2, then at the end of the loop the values of a and b will be xxx and yyy. 

Obviously with values that immediately prove the code is correct.

It happens quite often that the desired statement cannot be proven by induction directly - in this case giving the correct result fib (n) for some n doesn't imply the correct result fib (n+1) for the next larger n. You need to prove something about a and b.