examples/fib_memo.mlw

   1 (* Fibonacci function with memoisation *)
   2
   3 module FibMemo
   4
   5   use option.Option
   6   use int.Int
   7   use int.Fibonacci
   8   use ref.Ref
   9   use map.Map
  10
  11   type table = map int (option int)
  12
  13   predicate inv (t : table) =
  14     forall x y : int. t[x] = Some y -> y = fib x
  15
  16   val table : ref table
  17
  18   val add (x:int) (y:int) : unit
  19     writes  { table }
  20     ensures { !table = (old !table)[x <- Some y] }
  21
  22   exception Not_found
  23
  24   val find (x:int) : int
  25     ensures { !table[x] = Some result }
  26     raises  { Not_found -> !table[x] = None }
  27
  28   let rec fibo n =
  29     requires { 0 <= n /\ inv !table }
  30     ensures  { result = fib n /\ inv !table }
  31     variant  { 2*n }
  32     if n <= 1 then
  33       n
  34     else
  35       memo_fibo (n-1) + memo_fibo (n-2)
  36
  37   with memo_fibo n =
  38     requires { 0 <= n /\ inv !table }
  39     ensures  { result = fib n /\ inv !table }
  40     variant  { 2*n+1 }
  41     try  find n
  42     with Not_found -> let fn = fibo n in add n fn; fn end
  43
  44 end