examples/flexible_arrays.mlw

   1
   2 (** Flexible arrays implemented with Braun trees.
   3
   4   References:
   5   - W. Braun, M. Rem, A logarithmic implementation of flexible arrays.
   6     Memorandum MR83/4. Eindhoven University of Technology. 1983.
   7   - Hoogerwoord, R. R. A logarithmic implementation of flexible arrays.
   8     Conference on Mathematics of Program Construction. 1992.
   9   - Chris Okasaki. Three Algorithms on Braun Trees (Functional Pearl)
  10     J. Functional Programming 7 (6) 661–666. 1997
  11
  12   See also braun_trees.mlw for an implementation of priority queues using
  13   Braun trees (and a proof that a Braun tree has logarithmic height).
  14
  15   Author: Jean-Christophe Filliâtre (CNRS)
  16 *)
  17
  18 (** First, we work on bare Braun trees *)
  19
  20 module BraunTrees
  21
  22   use int.Int
  23   use int.ComputerDivision
  24   use export bintree.Tree
  25   use export bintree.Size
  26   use seq.Seq
  27
  28   predicate braun (t: tree 'a) = match t with
  29   | Empty      -> true
  30   | Node l _ r -> (size l = size r || size l = size r + 1) && braun l && braun r
  31   end
  32
  33   let rec function get_tree (t: tree 'a) (i: int) : 'a
  34     requires { 0 <= i < size t }
  35     requires { braun t }
  36     variant  { t }
  37   = match t with
  38     | Empty -> absurd
  39     | Node l x r ->
  40         if i = 0 then x else
  41         if mod i 2 = 1 then get_tree l (div i 2) else get_tree r (div i 2 - 1)
  42     end
  43
  44   let rec function set_tree (t: tree 'a) (i: int) (v: 'a) : (r: tree 'a)
  45     requires { 0 <= i < size t }
  46     requires { braun t }
  47     variant  { t }
  48     ensures  { size r = size t }
  49     ensures  { braun r }
  50     ensures  { get_tree r i = v }
  51     ensures  { forall j. 0 <= j < t.size -> j<>i -> get_tree r j = get_tree t j }
  52   = match t with
  53     | Empty -> absurd
  54     | Node l x r ->
  55         if i = 0 then Node l v r else
  56         if mod i 2 = 1 then Node (set_tree l (div i 2) v) x r
  57                        else Node l x (set_tree r (div i 2 - 1) v)
  58     end
  59
  60   let rec make_tree2 (n: int) (v: 'a) : (l: tree 'a, r: tree 'a)
  61     requires { n >= 0}
  62     variant { n }
  63     ensures { size l = n+1 && size r = n }
  64     ensures { braun l && braun r }
  65     ensures { forall i. 0 <= i < size l -> get_tree l i = v }
  66     ensures { forall i. 0 <= i < size r -> get_tree r i = v }
  67   = if n = 0 then
  68       Node Empty v Empty, Empty
  69     else if mod n 2 = 1 then
  70       let l, r = make_tree2 (div n 2) v in
  71       Node l v r, Node r v r
  72     else
  73       let l, r = make_tree2 (div n 2 - 1) v in
  74       Node l v l, Node l v r
  75
  76   let make_tree (n: int) (v: 'a) : (r: tree 'a)
  77     requires { n >= 0}
  78     ensures  { size r = n }
  79     ensures  { braun r }
  80     ensures  { forall i. 0 <= i < size r -> get_tree r i = v }
  81   = let _, r = make_tree2 n v in r
  82
  83   (* left insertion/removal *)
  84
  85   let rec cons_tree (v: 'a) (t: tree 'a) : (r: tree 'a)
  86     requires { braun t }
  87     variant  { t }
  88     ensures  { size r = size t + 1 }
  89     ensures  { braun r }
  90     ensures  { get_tree r 0 = v }
  91     ensures  { forall i. 0 <= i < size t -> get_tree r (i+1) = get_tree t i }
  92   = match t with
  93     | Empty      -> Node Empty v Empty
  94     | Node l x r -> Node (cons_tree x r) v l
  95     end
  96
  97   let rec tail_tree (t: tree 'a) : (r: tree 'a)
  98     requires { braun t }
  99     requires { size t > 0 }
 100     variant  { t }
 101     ensures  { size r = size t - 1 }
 102     ensures  { braun r }
 103     ensures  { forall i. 0 < i < size t -> get_tree r (i-1) = get_tree t i }
 104   = match t with
 105     | Empty              -> absurd
 106     | Node Empty _ Empty -> Empty
 107     | Node l     _ r     -> Node r (get_tree l 0) (tail_tree l)
 108     end
 109
 110   (* right insertion/removal *)
 111
 112   let rec snoc_tree (s: int) (t: tree 'a) (v: 'a) : (r: tree 'a)
 113     requires { braun t }
 114     requires { s = size t }
 115     variant  { t }
 116     ensures  { size r = size t + 1 }
 117     ensures  { braun r }
 118     ensures  { forall i. 0 <= i < size t -> get_tree r i = get_tree t i }
 119     ensures  { get_tree r s = v }
 120   = match t with
 121   | Empty      -> Node Empty v Empty
 122   | Node l x r -> if mod s 2 = 1 then Node (snoc_tree (div s 2) l v) x r
 123                                  else Node l x (snoc_tree (div s 2 - 1) r v)
 124   end
 125
 126   let rec liat_tree (s: int) (t: tree 'a) : (r: tree 'a)
 127     requires { braun t }
 128     requires { s = size t > 0 }
 129     variant  { t }
 130     ensures  { size r = size t - 1 }
 131     ensures  { braun r }
 132     ensures  { forall i. 0 <= i < size r -> get_tree r i = get_tree t i }
 133   = match t with
 134     | Empty -> absurd
 135     | Node Empty _ Empty -> Empty
 136     | Node l     x r     -> if mod s 2 = 0 then Node (liat_tree (div s 2) l) x r
 137                                            else Node l x (liat_tree (div s 2) r)
 138    end
 139
 140   (* TODO: Okasaki's of_list *)
 141
 142 end
 143
 144 (** Second, we encapsulate Braun trees in a record, together with its
 145   size and suitable invariants. *)
 146
 147 module FlexibleArrays
 148
 149   use int.Int
 150   use BraunTrees as B
 151
 152   type t 'a = {
 153     size: int;
 154     tree: B.tree 'a;
 155   }
 156   invariant { B.braun tree }
 157   invariant { B.size tree = size >= 0 }
 158
 159   let constant empty : t 'a
 160   = { size = 0; tree = B.Empty }
 161     ensures { result.size = 0 }
 162
 163   let function get (t: t 'a) (i: int) : 'a
 164     requires { 0 <= i < t.size }
 165   = B.get_tree t.tree i
 166
 167   let set (t: t 'a) (i: int) (v: 'a) : (r: t 'a)
 168     requires { 0 <= i < t.size }
 169     ensures  { r.size = t.size }
 170     ensures  { get r i = v }
 171     ensures  { forall j. 0 <= j < t.size -> j<>i -> get r j = get t j }
 172   = { size = t.size; tree = B.set_tree t.tree i v }
 173
 174   let make_tree (n: int) (v: 'a) : (r: t 'a)
 175     requires { n >= 0}
 176     ensures  { r.size = n }
 177     ensures  { forall i. 0 <= i < r.size -> get r i = v }
 178   = { size = n; tree = B.make_tree n v }
 179
 180   (* left insertion/removal *)
 181
 182   let cons (v: 'a) (t: t 'a) : (r: t 'a)
 183     ensures  { size r = size t + 1 }
 184     ensures  { get r 0 = v }
 185     ensures  { forall i. 0 <= i < t.size -> get r (i+1) = get t i }
 186   = { size = t.size + 1; tree = B.cons_tree v t.tree }
 187
 188   let tail (t: t 'a) : (r: t 'a)
 189     requires { t.size > 0 }
 190     ensures  { r.size = t.size - 1 }
 191     ensures  { forall i. 0 < i < size t -> get r (i-1) = get t i }
 192   = { size = t.size - 1; tree = B.tail_tree t.tree }
 193
 194   (* right insertion/removal *)
 195
 196   let snoc (t: t 'a) (v: 'a) : (r: t 'a)
 197     ensures  { r.size = t.size + 1 }
 198     ensures  { forall i. 0 <= i < t.size -> get r i = get t i }
 199     ensures  { get r t.size = v }
 200   = { size = t.size + 1; tree = B.snoc_tree t.size t.tree v }
 201
 202   let liat (t: t 'a) : (r: t 'a)
 203     requires { t.size > 0 }
 204     ensures  { r.size = t.size - 1 }
 205     ensures  { forall i. 0 <= i < r.size -> get r i = get t i }
 206   = { size = t.size - 1; tree = B.liat_tree t.size t.tree }
 207
 208 end