examples_in_progress/flexible_array.mlw

   1
   2 (** Flexible arrays
   3
   4     Flexible arrays are arrays whose size can be changed by adding or
   5     removing elements at either end (one at a time).
   6
   7     This is an implementation of flexible arrays using Braun trees,
   8     following
   9
  10       Rob Hoogerwoord
  11       A logarithmic implementation of flexible arrays
  12       http://alexandria.tue.nl/repository/notdare/772185.pdf
  13
  14     All operations (get, set, le, lr, he, hr) have logarithmic complexity.
  15
  16     Note: Braun trees can also be used to implement priority queues.
  17     See braun_trees.mlw. This file also contains a proof that Braun
  18     trees have logarithmic height.
  19
  20     Author: Jean-Christophe Filliâtre (CNRS)
  21 *)
  22
  23 module FlexibleArray
  24
  25   use int.Int
  26   use int.ComputerDivision
  27   use bintree.Tree
  28   use export bintree.Size
  29   use ref.Ref
  30   use import seq.Seq as S
  31   use import queue.Queue as Q
  32   use list.List
  33   use seq.Mem
  34
  35   (* to be a Braun tree *)
  36   predicate inv (t: tree 'a) = match t with
  37   | Empty      -> true
  38   | Node l _ r -> (size l = size r || size l = size r + 1) && inv l && inv r
  39   end
  40
  41   type t 'a = {
  42     length: int;
  43       tree: tree 'a;
  44   } invariant {
  45     length = size tree && inv tree
  46   }
  47
  48   let empty () : t 'a
  49     ensures { result.length = 0 }
  50     = { length = 0; tree = Empty }
  51
  52   let is_empty (t: t 'a) : bool
  53     ensures  { result <-> t.length = 0 }
  54   =
  55     t.length = 0
  56
  57   let rec function get_aux (t: tree 'a) (i: int) : 'a
  58     requires { 0 <= i < size t }
  59     requires { inv t }
  60     variant  { t }
  61   = match t with
  62     | Empty -> absurd
  63     | Node l x r ->
  64        if i = 0 then x
  65        else if mod i 2 = 1 then get_aux l (div i 2) else get_aux r (div i 2 - 1)
  66     end
  67
  68   let function get (t: t 'a) (i: int) : 'a
  69     requires { 0 <= i < t.length }
  70   = get_aux t.tree i
  71
  72   let rec set_aux (t: tree 'a) (i: int) (v: 'a) : tree 'a
  73     requires { 0 <= i < size t }
  74     requires { inv t }
  75     variant  { t }
  76     ensures  { inv result }
  77     ensures  { size result = size t }
  78     ensures  { forall j. 0 <= j < size t -> j <> i ->
  79                get_aux result j = get_aux t j }
  80     ensures  { get_aux result i = v }
  81   = match t with
  82     | Empty -> absurd
  83     | Node l x r ->
  84        if i = 0 then Node l v r
  85        else if mod i 2 = 1 then Node (set_aux l (div i 2) v) x r
  86        else Node l x (set_aux r (div i 2 - 1) v)
  87     end
  88
  89   let set (t: t 'a) (i: int) (v: 'a) : t 'a
  90     requires { 0 <= i < t.length }
  91     ensures  { result.length = t.length }
  92     ensures  { forall j. 0 <= j < t.length -> j <> i -> get result j = get t j }
  93     ensures  { get result i = v }
  94   = { length = t.length; tree = set_aux t.tree i v }
  95
  96   (* low extension *)
  97   let rec le_aux (v: 'a) (t: tree 'a) : tree 'a
  98     requires { inv t }
  99     variant  { t }
 100     ensures  { inv result }
 101     ensures  { size result = size t + 1 }
 102     ensures  { get_aux result 0 = v }
 103     ensures  { forall j. 0 <= j < size t ->
 104                get_aux result (j + 1) = get_aux t j }
 105   = match t with
 106     | Empty -> Node Empty v Empty
 107     | Node l x r -> Node (le_aux x r) v l
 108     end
 109
 110   let rec le (v: 'a) (t: t 'a) : t 'a
 111     ensures  { result.length = t.length + 1 }
 112     ensures  { get result 0 = v }
 113     ensures  { forall j. 0 <= j < t.length -> get result (j + 1) = get t j }
 114   = { length = t.length + 1; tree = le_aux v t.tree }
 115
 116   (* low removal *)
 117   let rec lr_aux (t: tree 'a) : tree 'a
 118     requires { inv t }
 119     requires { size t > 0 }
 120     variant  { t }
 121     ensures  { inv result }
 122     ensures  { size result = size t - 1 }
 123     ensures  { forall j. 0 <= j < size result ->
 124                get_aux result j = get_aux t (j + 1) }
 125   = match t with
 126     | Empty -> absurd
 127     | Node Empty _ Empty -> Empty
 128     | Node l _ r -> Node r (get_aux l 0) (lr_aux l)
 129     end
 130
 131   let lr (t: t 'a) : t 'a
 132     requires { t.length > 0 }
 133     ensures  { result.length = t.length - 1 }
 134     ensures  { forall j. 0 <= j < result.length ->
 135                get result j = get t (j + 1) }
 136   = { length = t.length - 1; tree = lr_aux t.tree }
 137
 138   (* high extension *)
 139   let rec he_aux (s: int) (t: tree 'a) (v: 'a) : tree 'a
 140     requires { inv t }
 141     requires { s = size t }
 142     variant  { t }
 143     ensures  { inv result }
 144     ensures  { size result = size t + 1 }
 145     ensures  { get_aux result (size t) = v }
 146     ensures  { forall j. 0 <= j < size t -> get_aux result j = get_aux t j }
 147   = match t with
 148     | Empty -> Node Empty v Empty
 149     | Node l x r -> if mod s 2 = 1 then Node (he_aux (div s 2) l v) x r
 150                                    else Node l x (he_aux (div s 2 - 1) r v)
 151     end
 152
 153   let he (t: t 'a) (v: 'a) : t 'a
 154     ensures  { result.length = t.length + 1 }
 155     ensures  { get result t.length = v }
 156     ensures  { forall j. 0 <= j < t.length -> get result j = get t j }
 157   =
 158     { length = t.length + 1; tree = he_aux t.length t.tree v }
 159
 160   (* high removal *)
 161   let rec hr_aux (s: int) (t: tree 'a) : tree 'a
 162     requires { inv t }
 163     requires { s = size t > 0 }
 164     variant  { t }
 165     ensures  { inv result }
 166     ensures  { size result = size t - 1 }
 167     ensures  { forall j. 0 <= j < size result ->
 168                get_aux result j = get_aux t j }
 169   = match t with
 170     | Empty -> absurd
 171     | Node Empty _ Empty -> Empty
 172     | Node l x r -> if mod s 2 = 0 then Node (hr_aux (div s 2) l) x r
 173                                    else Node l x (hr_aux (div s 2) r)
 174     end
 175
 176   let hr (t: t 'a) : t 'a
 177     requires { t.length > 0 }
 178     ensures  { result.length = t.length - 1 }
 179     ensures  { forall j. 0 <= j < result.length -> get result j = get t j }
 180   =
 181     { length = t.length - 1; tree = hr_aux t.length t.tree }
 182
 183   (* the sequence of elements, in order *)
 184
 185   function interleave (x y: seq 'a) : seq 'a =
 186     S.create
 187       (S.length x + S.length y)
 188       (fun i -> if mod i 2 = 0 then x[div i 2] else y[div i 2])
 189
 190   function elements_aux (t: tree 'a): seq 'a =
 191     match t with
 192     | Empty -> S.empty
 193     | Node l x r -> cons x (interleave (elements_aux l) (elements_aux r))
 194     end
 195
 196   let rec lemma elements_aux_length (t: tree 'a)
 197     variant  { t }
 198     ensures  { S.length (elements_aux t) = size t }
 199   = match t with
 200     | Empty -> ()
 201     | Node l _ r -> elements_aux_length l; elements_aux_length r
 202     end
 203
 204   let rec lemma elements_aux_correct (t: tree 'a) (i: int)
 205     requires { 0 <= i < size t }
 206     requires { inv t }
 207     variant  { t }
 208     ensures  { (elements_aux t)[i] = get_aux t i }
 209   = match t with
 210     | Empty -> ()
 211     | Node l _ r ->
 212         elements_aux_length l; elements_aux_length r;
 213         if i = 0 then () else
 214         if mod i 2 = 1 then elements_aux_correct l (div i 2)
 215                        else elements_aux_correct r (div i 2 - 1)
 216     end
 217
 218   function elements (a: t 'a) : seq 'a =
 219     elements_aux a.tree
 220
 221   lemma elements_correct:
 222     forall a: t 'a.
 223     S.length (elements a) = a.length /\
 224     forall i. 0 <= i < a.length -> (elements a)[i] = get a i
 225
 226   (* traversing the elements, in order, in linear time *)
 227
 228   let non_empty (t: tree 'a) : bool
 229     ensures { result <-> t <> Empty }
 230   = match t with
 231     | Empty      -> false
 232     | Node _ _ _ -> true
 233     end
 234
 235   use int.Sum
 236
 237   function size_list (l: seq (tree 'a)) : int =
 238     sum (fun i -> size l[i]) 0 (Seq.length l)
 239
 240   let lemma size_list_nonneg (l: seq (tree 'a)) : unit
 241     ensures { size_list l >= 0 }
 242   = ()(* match l with Nil -> () | Cons _ s -> size_list_nonneg s end *)
 243
 244   let lemma size_list_append (l1 l2: seq (tree 'a)) : unit
 245     ensures { size_list (l1 ++ l2) = size_list l1 + size_list l2 }
 246   = ()(* match l1 with Nil -> () | Cons _ s1 -> size_list_append s1 l2 end *)
 247
 248   lemma size_list_snoc:
 249     forall l: seq (tree 'a), t: tree 'a.
 250     size_list (l ++ cons t empty) = size_list l + size t
 251
 252   (* FIXME: In practice, such a function iter would have a visitor function
 253      as argument. Here, we only intend to prove the soundness of such
 254      an iteration. So we simply store the visited elements in a ghost
 255      sequence and then prove at this end that this sequence is in order,
 256      with an assertion. *)
 257
 258   let iter (a: t 'a) : unit =
 259     let ghost visited = ref S.empty in
 260     let q = Q.create () in
 261     let left = Q.create () in
 262     let right = Q.create () in
 263     if non_empty a.tree then begin
 264       Q.push a.tree q;
 265       while not (Q.is_empty q) do
 266         invariant { not (mem Empty q) }
 267         invariant { not (mem Empty left) }
 268         invariant { not (mem Empty right) }
 269         invariant { S.length !visited + size_list q +
 270                     size_list left + size_list right = a.length }
 271         invariant { forall i. 0 <= i < S.length !visited ->
 272                     !visited[i] = get a i }
 273         invariant { S.length q = 0 -> S.length left = S.length right = 0 }
 274         variant   { a.length - S.length !visited }
 275         let x = Q.safe_pop q in
 276         match x with
 277           | Empty -> absurd
 278           | Node l y r ->
 279             (* visit y here *)
 280             ghost visited := snoc !visited y;
 281             if non_empty l then Q.push l left;
 282             if non_empty r then Q.push r right;
 283         end;
 284         if Q.is_empty q then begin
 285           Q.transfer right left;
 286           Q.transfer left q;
 287         end
 288       done
 289     end;
 290     assert { forall i. 0 <= i < a.length -> !visited[i] = get a i }
 291
 292 end