Past exam of the year 1 of the computer science course of the University of Oxford / 2005 / Functional programming, data structures and algorithms, procedural programming, and digital hardware / 6 / a / Solution

An Oberon recursive procedure can implement the defining recurrence relation directly. Its precondition is $n\ge 1$; arithmetic is assumed to remain in the representable integer range.

PROCEDURE Fib(n: INTEGER): INTEGER;
  VAR result: INTEGER;
BEGIN
  IF n <= 2 THEN
    result := 1
  ELSE
    result := Fib(n-1) + Fib(n-2)
  END;
  RETURN result
END Fib;

Correctness follows by strong induction: the two base inputs give $1$, and for $n>2$ the returned sum is $F_{n-1}+F_{n-2}=F_n$. On each recursive branch the positive integer argument strictly decreases, while recursion stops at $1$ or $2$. The well-ordering principle therefore proves algorithm termination.The method repeats many subproblems and has exponential time complexity; termination alone does not make it efficient.