This article is one of some topics from my lecture Design and Analysis of Algorithm (see here). The goal is to understand how to prove the correctness of an algorithm in iterative form. Let’s start with the simple one.

Problem

Given an algorithm  to find the Fibonacci number at n sequence. As its definition, Fibonacci sequence is defined as .

Can you prove the following Fibonacci algorithm is correct?

Function Fib(n)
  a=0; b=1; i=2
  while ( i <= n)
      c=a+b
      a=b
      b=c
      i=i+1
  endwhile
  return b
end

In order to prove the correctness of above algorithm mathematically, according Ian Parberry and William Gasarch (see his lecture note), then some steps should be considered  as follows:

1. Claim the problem
2. List the fact about algorithm
3. Define the loop invariant and prove it by using mathematical induction method
4. Make a conclusion

 

Solution

1.Claim: function fib(n) return

2. Fact about algorithm:

for iteration 0 (j=0), then

for iteration j+1, then

3. Loop Invariant

Then proving the loop invariant by using mathematical induction.

proof

Basis: at j=0, then  holds.

Induction: Assume that at j=k, it is true that

and then it will be proved that at j=k+1, the following relation is hold.

Then it can be

holds

holds.

holds

4. Conclusion

Claim that b will return

First look at algorithm, the loop process will terminate at i=n+1.

Assume that the termination of this algorithm (loop process) is at t iteration, then by using loop invariant we got

termination:

Therefore we have ,

and the prove is done.