ProVal

(* Fibonacci function with memoisation *)

module M

  use import int.Int
  use import ref.Ref

  function fib int : int

  axiom Fib_def : forall n:int. fib n =
     if n <= 1 then 1 else fib (n-1) + fib (n-2)

  type option 'a = None | Some 'a

  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 reads { table }
    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 }
    if n <= 1 then
      1
    else
      memo_fibo (n-1) + memo_fibo (n-2)

  with memo_fibo n =
    requires { 0 <= n /\ inv !table }
    ensures { result = fib n /\ inv !table }
    try  find n
    with Not_found -> let fn = fibo n in add n fn; fn end

end