Fibonacci with memoization
Computing the Fibonacci function using memoization.
There is no implementation for the memoization table, only parameters.
Auteurs: Jean-Christophe Filliâtre
Catégories: Mathematics
Outils: Why3
Voir aussi: Fibonacci sequence, linear algorithm, Java version / Fibonacci function, linear/logarithmic algorithms, Why3 version
see also the index (by topic, by tool, by reference, by year)
(* Fibonacci function with memoisation *) module FibMemo use option.Option use int.Int use int.Fibonacci use ref.Ref use map.Map type table = map int (option int) predicate inv (t : table) = forall x y : int. t[x] = Some y -> y = fib x val table : ref table val add (x:int) (y:int) : unit writes { table } ensures { !table = (old !table)[x <- Some y] } exception Not_found val find (x:int) : int ensures { !table[x] = Some result } raises { Not_found -> !table[x] = None } let rec fibo n = requires { 0 <= n /\ inv !table } ensures { result = fib n /\ inv !table } variant { 2*n } if n <= 1 then n else memo_fibo (n-1) + memo_fibo (n-2) with memo_fibo n = requires { 0 <= n /\ inv !table } ensures { result = fib n /\ inv !table } variant { 2*n+1 } try find n with Not_found -> let fn = fibo n in add n fn; fn end end
download ZIP archive