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
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
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.)
Try to
So
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.