Prove correctness of the following algorithm for computing Fibonacci numbers

Question

I am a student studying for my BS in Computer Science. We recently got asked this question in on of my class and with no book to reference I am going to ask it here for a little help. I know I will have to use induction but I don't really understand how

Input: a, a natural number
Output: F_a, the ath Fibonacci number
Let i=1
While i<=a do
  if i=1 or i=2, then Fib(i)<-1
  else Fib(i)<-Fib(i-1)+ Fib(i-2)
  i <- i+1
end
Print Fib(a)

Answer 1

I think you might be overthinking the problem. The induction is pretty simple; let's go through the steps:

Base case: The algorithm correctly puts Fib(1) = 1, Fib(2) = 1.

(Strong) Inductive step: Suppose the algorithm correctly calculates the values for Fibonacci numbers up to $k$.

Then, it puts Fib(k+1) = Fib(k) + Fib(k-1), so the value of Fib(k+1) is correctly calculated too.

Answer 2

Input: a, a natural number
Output: F_a, the a'th Fibonacci number

1 Let i = 1
2
3 While i <= a do
4    
5  if i = 1 or i = 2 then Fib[i] <- 1
6
7  else Fib[i] <- Fib[i - 1] + Fib[i - 2]
8
9  i <- i + 1
10
11 end
12
13 Print Fib[a]

First determine what you are trying to prove:

At line 12, $\operatorname{Fib}[a] = F_a$

Now consider some assumptions you will need to prove it: $$F_a = F_{a - 1} + F_{a - 2}$$ $$F_1 = 1$$ $$F_2 = 1$$

To prove this kind of statement, you need to establish what is called a loop invariant. This is a statement for which, if it is true at the start of 1 pass of the loop (line 4), then it is true at the end of that pass of the loop (line 10). Here your primary loop invariant is:

$$\forall j ~:~ 1 \le j < i \implies \operatorname{Fib}[j] = F_j \tag{L}$$

After using the definition of the fibonacci sequence to prove that (L) is a loop invariant, if you can prove that (L) holds at line 2 (before the loop) then it must hold at line 12 (after the loop).

Furthermore, the loop condition at line 3 implies that at line 12 $\lnot (i \le a)$.

So you are left with two statements being true at line 12:

$$\begin{cases} \forall j ~:~ 1 \le j < i \implies \operatorname{Fib}[j] = F_j \\ i > a \end{cases}$$

Those two together are enough to establish that at line 12, $\operatorname{Fib}[a] = F_a$.

To prove that the program terminates, you need to establish a decreasing ordinal during the loop. So to establish halting you need to prove that $a - i + 1$ is always positive and decreasing during the loop.

Aside, this is also why most people don't bother attempting to prove things about procedural programs, but rather prefer functional programs.