Fibonacci sequence, linear algorithm, Java version
Computation of Fibonacci numbers using an algorithm with linear complexity.
Auteurs: Claude Marché
Catégories: Inductive predicates / Arithmetic
Voir aussi: 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;
}
}