Wiki Agenda Contact Version française

Fibonacci sequence, linear algorithm, Java version

Computation of Fibonacci numbers using an algorithm with linear complexity.


Authors: Claude Marché

Topics: Inductive predicates / Mathematics

Tools: Krakatoa / Coq

See also: Fibonacci with memoization / Fibonacci function, linear/logarithmic algorithms, Why3 version

see also the index (by topic, by tool, by reference, by year)


Description

The Fibonacci sequence is definition recursively by F(0)=0, F(1)=1, F(n+2)=F(n+1)+F(n). Is is formalized below by a predicate isFib(x,r) meant to be true whenever r is F(n), it is defined inductively.

The Java code implements a reasonably efficient algorithm for computing F(n) in a time linear in n. (There exist algorithms in logarithmic time).

The lemmas are just there to experiment with the inductive predicate, and to test the efficiency of provers.

Proof

The proof is the Java method is done automatically for SMT solvers. On the other hand, the lemmas are not, probably because the depth of instantiation of quantified axioms is too high.


// int model: unbounded mathematical integers
//@+ CheckArithOverflow = no

/*@ inductive isfib(integer x, integer r) {
  @  case isfib0: isfib(0,0);
  @  case isfib1: isfib(1,1);
  @  case isfibn: 
  @   \forall integer n r p; 
  @     n >= 2 && isfib(n-2,r) && isfib(n-1,p) ==> isfib(n,p+r);
  @ }
  @*/ 

//@ lemma isfib_2_1 : isfib(2,1);
//@ lemma isfib_6_8 : isfib(6,8);

// provable only if def is inductive (least fix point)
//@ lemma not_isfib_2_2 : ! isfib(2,2);

public class Fibonacci {

    /*@ requires n >= 0;
      @ ensures isfib(n, \result); 
      @*/
    public static long Fib(int n) {
	long y=0, x=1, aux;

	/*@ loop_invariant 0 <= i <= n && isfib(i+1,x) && isfib(i,y);
	  @ loop_variant n-i;
	  @*/
	for(int i=0; i < n; i++) {
	    aux = y;
	    y = x;
	    x = x + aux;
	}
	return y;
    }
}