fib_memo.mlw 934 Bytes
Newer Older
1 2
(* Fibonacci function with memoisation *)

3
module FibMemo
4

5 6 7 8 9
  use option.Option
  use int.Int
  use int.Fibonacci
  use ref.Ref
  use map.Map
10

11
  type table = map int (option int)
12

Andrei Paskevich's avatar
Andrei Paskevich committed
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 19
  val add (x:int) (y:int) : unit
    writes  { table }
20
    ensures { !table = (old !table)[x <- Some y] }
21 22 23

  exception Not_found

Andrei Paskevich's avatar
Andrei Paskevich committed
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 31
    ensures  { result = fib n /\ inv !table }
    variant  { 2*n }
32
    if n <= 1 then
33
      n
34
    else
35 36 37
      memo_fibo (n-1) + memo_fibo (n-2)

  with memo_fibo n =
38
    requires { 0 <= n /\ inv !table }
39 40
    ensures  { result = fib n /\ inv !table }
    variant  { 2*n+1 }
41 42 43 44
    try  find n
    with Not_found -> let fn = fibo n in add n fn; fn end

end