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
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.
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.