## Fibonacci with memoization

Computing the Fibonacci function using memoization.

There is no implementation for the memoization table, only parameters.

**Authors:** Jean-Christophe Filliâtre

**Topics:** Mathematics

**Tools:** Why3

**See also:** 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 import option.Option use import int.Int use import int.Fibonacci use import ref.Ref use import map.Map as M type table = M.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