vacid_0_red_black_trees.mlw 9.67 KB
Newer Older
1

2
module RedBlackTree
3

4
  (* Red-black trees (data type) *)
5

6 7 8 9 10 11
  type key = int
  type value = int

  type color = Red | Black

  type tree =
12
    | Leaf
13
    | Node color tree key value tree
14

15 16
  (* occurrence of a key/value pair in a tree *)

17
  predicate memt (t : tree) (k : key) (v : value) =
18 19
    match t with
    | Leaf -> false
20
    | Node _ l k' v' r -> (k = k' /\ v = v') \/ memt l k v \/ memt r k v
21
    end
22

23 24 25 26
  lemma memt_color :
    forall l r : tree, k k' : key, v v' : value, c c' : color.
    memt (Node c l k v r) k' v' -> memt (Node c' l k v r) k' v'

27 28
  (* binary search tree *)

29
  use int.Int
30

31
  predicate lt_tree (x : key) (t : tree) =
32 33
    forall k : key. forall v : value. memt t k v -> k < x

34
  predicate gt_tree (x : key) (t : tree) =
35 36
    forall k : key. forall v : value. memt t k v -> x < k

37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
  lemma lt_leaf: forall x: key. lt_tree x Leaf

  lemma gt_leaf: forall x: key. gt_tree x Leaf

  lemma lt_tree_node:
    forall x y: key, v: value, l r: tree, c: color.
    lt_tree x l -> lt_tree x r -> y < x -> lt_tree x (Node c l y v r)

  lemma gt_tree_node:
    forall x y: key, v: value, l r: tree, c: color.
    gt_tree x l -> gt_tree x r -> x < y -> gt_tree x (Node c l y v r)

  lemma lt_node_lt:
    forall x y: key, v: value, l r: tree, c: color.
    lt_tree x (Node c l y v r) -> y < x

  lemma gt_node_gt:
    forall x y: key, v: value, l r: tree, c: color.
    gt_tree x (Node c l y v r) -> x < y

  lemma lt_left:
    forall x y: key, v: value, l r: tree, c : color.
    lt_tree x (Node c l y v r) -> lt_tree x l

  lemma lt_right:
    forall x y: key, v: value,  l r: tree, c: color.
    lt_tree x (Node c l y v r) -> lt_tree x r

  lemma gt_left:
    forall x y: key, v: value, l r: tree, c: color.
    gt_tree x (Node c l y v r) -> gt_tree x l

  lemma gt_right:
    forall x y: key, v: value, l r: tree, c: color.
    gt_tree x (Node c l y v r) -> gt_tree x r

  lemma lt_tree_not_in:
    forall x: key, t: tree. lt_tree x t -> forall v: value. not (memt t x v)

  lemma lt_tree_trans:
    forall x y: key. x < y -> forall t: tree. lt_tree x t -> lt_tree y t

  lemma gt_tree_not_in :
    forall x: key, t: tree. gt_tree x t -> forall v: value. not (memt t x v)

  lemma gt_tree_trans :
    forall x y: key. y < x -> forall t: tree. gt_tree x t -> gt_tree y t

85
  predicate bst (t : tree) =
86 87
    match t with
    | Leaf -> true
88
    | Node _ l k _ r -> bst l /\ bst r /\ lt_tree k l /\ gt_tree k r
89 90 91 92
    end

  lemma bst_Leaf : bst Leaf

93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
  lemma bst_left:
    forall k: key, v: value, l r: tree, c: color. bst (Node c l k v r) -> bst l

  lemma bst_right:
    forall k: key, v: value, l r: tree, c: color. bst (Node c l k v r) -> bst r

  lemma bst_color:
    forall c c': color, k: key, v: value, l r: tree.
    bst (Node c l k v r) -> bst (Node c' l k v r)

  lemma rotate_left:
    forall kx ky: key, vx vy: value, a b c: tree, c1 c2 c3 c4: color.
    bst (Node c1 a kx vx (Node c2 b ky vy c)) ->
    bst (Node c3 (Node c4 a kx vx b) ky vy c)

  lemma rotate_right:
    forall kx ky: key, vx vy: value, a b c: tree, c1 c2 c3 c4: color.
    bst (Node c3 (Node c4 a kx vx b) ky vy c) ->
    bst (Node c1 a kx vx (Node c2 b ky vy c))

113
  (* [rbtree n t]: red black tree invariant
114 115 116
     [t] is a properly balanced red-black tree, i.e. it
      satisfies the following two invariants:
      - a red node has no red son
117
      - any path from the root to a leaf has exactly [n] black nodes
118
   *)
119

120
  predicate is_not_red (t : tree) =
121 122 123 124 125
    match t with
    | Node Red _ _ _ _ -> false
    | Leaf | Node Black _ _ _ _ -> true
    end

126
  predicate rbtree (n : int) (t : tree) =
127
    match t with
128
    | Leaf ->
129
        n = 0
130
    | Node Red   l _ _ r ->
131
        rbtree n l /\ rbtree n r /\ is_not_red l /\ is_not_red r
132
    | Node Black l _ _ r ->
133
        rbtree (n-1) l /\ rbtree (n-1) r
134 135
    end

136 137
  lemma rbtree_Leaf:
    rbtree 0 Leaf
138

139
  lemma rbtree_Node1:
140 141
    forall k:key, v:value. rbtree 0 (Node Red Leaf k v Leaf)

142 143 144 145 146 147 148 149
  lemma rbtree_left:
    forall x: key, v: value, l r: tree, c: color.
    (exists n: int. rbtree n (Node c l x v r)) -> exists n: int. rbtree n l

  lemma rbtree_right:
    forall x: key, v: value, l r: tree, c: color.
    (exists n: int. rbtree n (Node c l x v r)) -> exists n: int. rbtree n r

150 151 152 153
  (* lookup *)

  exception Not_found

154 155
  let rec find (t : tree) (k : key) : value
    requires { bst t }
156
    variant { t }
157 158 159
    ensures { memt t k result }
    raises { Not_found -> forall v : value. not (memt t k v) }
  = match t with
160
    | Leaf -> raise Not_found
161 162
    | Node _ l k' v r ->
        if k = k' then v
163 164 165 166 167
        else if k < k' then find l k
        else (* k > k' *) find r k
    end

  (* insertion *)
168

169 170
  (** `almost_rbtree n t`: `t` may have one red-red conflict at its root;
      it satisfies `rbtree n` everywhere else *)
171

172
  predicate almost_rbtree (n : int) (t : tree) =
173
    match t with
174
    | Leaf ->
175
        n = 0
176
    | Node Red   l _ _ r ->
177
        rbtree n l /\ rbtree n r
178
    | Node Black l _ _ r ->
179
        rbtree (n-1) l /\ rbtree (n-1) r
180
    end
181

182 183 184 185 186 187 188 189 190 191 192
  lemma rbtree_almost_rbtree:
    forall n: int, t: tree. rbtree n t -> almost_rbtree n t

  lemma rbtree_almost_rbtree_ex:
    forall s: tree.
    (exists n: int. rbtree n s) -> exists n: int. almost_rbtree n s

  lemma almost_rbtree_rbtree_black:
    forall x: key, v: value, l r: tree, n: int.
    almost_rbtree n (Node Black l x v r) -> rbtree n (Node Black l x v r)

193 194
  (** `lbalance c x l r` acts as a black node constructor,
      solving a possible red-red conflict on `l`, using the following
195 196
      schema:

197
      B (R (R a x b) y c) z d
198 199
      B (R a x (R b y c)) z d -> R (B a x b) y (R c z d)
      B a x b -> B a x b
200 201 202

      The result is not necessarily a black node. *)

203 204 205 206 207 208 209 210 211
  let lbalance (l : tree) (k : key) (v : value) (r : tree)
    requires { lt_tree k l /\ gt_tree k r /\ bst l /\ bst r }
    ensures { bst result /\
      (forall n : int. almost_rbtree n l -> rbtree n r -> rbtree (n+1) result)
      /\
      forall k':key, v':value.
        memt result k' v' <->
        if k' = k then v' = v else (memt l k' v' \/ memt r k' v') }
  = match l with
212
    | Node Red (Node Red a kx vx b) ky vy c
213
    | Node Red a kx vx (Node Red b ky vy c) ->
214
        Node Red (Node Black a kx vx b) ky vy (Node Black c k v r)
215
    | _ ->
216
        Node Black l k v r
217
    end
218

219 220
  (** `rbalance l x r` is similar to `lbalance`, solving a possible red-red
      conflict on `r`. The balancing schema is similar:
221 222

      B a x (R (R b y c) z d)
223 224
      B a x (R b y (R c z d)) -> R (B a x b) y (R c z d)
      B a x b -> B a x b
225 226
   *)

227 228 229 230 231 232 233 234 235
  let rbalance (l : tree) (k : key) (v : value) (r : tree)
    requires { lt_tree k l /\ gt_tree k r /\ bst l /\ bst r }
    ensures { bst result /\
      (forall n : int. almost_rbtree n r -> rbtree n l -> rbtree (n+1) result)
      /\
      forall k':key, v':value.
        memt result k' v' <->
        if k' = k then v' = v else (memt l k' v' \/ memt r k' v') }
  = match r with
236
    | Node Red (Node Red b ky vy c) kz vz d
237
    | Node Red b ky vy (Node Red c kz vz d) ->
238
        Node Red (Node Black l k v b) ky vy (Node Black c kz vz d)
239
    | _ ->
240
        Node Black l k v r
241
    end
242

243 244
  (* `insert x s` inserts `x` in tree `s`, resulting in a possible top red-red
     conflict when `s` is red. *)
245

246 247
  let rec insert (t : tree) (k : key) (v : value) : tree
    requires { bst t /\ exists n: int. rbtree n t }
248
    variant { t }
249 250 251 252 253 254 255
    ensures { bst result /\
      (forall n : int. rbtree n t -> almost_rbtree n result /\
         (is_not_red t -> rbtree n result)) /\
      memt result k v /\
      forall k':key, v':value.
      memt result k' v' <-> if k' = k then v' = v else memt t k' v' }
  = match t with
256 257 258 259 260 261 262 263 264 265 266 267
    | Leaf ->
        Node Red Leaf k v Leaf
    | Node Red l k' v' r ->
        if k < k' then Node Red (insert l k v) k' v' r
        else if k' < k then Node Red l k' v' (insert r k v)
        else (* k = k' *) Node Red l k' v r
    | Node Black l k' v' r ->
        if k < k' then lbalance (insert l k v) k' v' r
        else if k' < k then rbalance l k' v' (insert r k v)
        else (* k = k' *) Node Black l k' v r
    end

268
  (* finally `add x s` calls `insert` and recolors the root as black *)
269

270 271 272
  let add (t : tree) (k : key) (v : value) : tree
    requires { bst t /\ exists n:int. rbtree n t }
    ensures { bst result /\ (exists n:int. rbtree n result) /\
273
      memt result k v /\
274
      forall k':key, v':value.
275
      memt result k' v' <-> if k' = k then v' = v else memt t k' v' }
276 277 278 279
  = match insert t k v with
    | Node _ l k' v' r -> Node Black l k' v' r
    | Leaf -> absurd
    end
280

281 282 283 284
end

module Vacid0

285
  (* the VACID-0 interface = mutable map with default value*)
286

287 288
  use ref.Ref
  use RedBlackTree
289

290 291
  type rbt = (value, tree)

292 293
  predicate inv (r : rbt) =
    let (_, t) = r in bst t /\ exists n : int. rbtree n t
294

295
  let function default (r : rbt) : value =
296 297
    let (d, _) = r in d

298
  predicate mem (r : rbt) (k : key) (v : value) =
299
    let (d, t) = r in
300
    memt t k v \/ (v = d /\ forall v':value. not (memt t k v'))
301

302 303
  let create (d : int)
    ensures { inv !result /\
304
      default !result = d /\
305
      forall k:key, v:value. mem !result k v <-> v = d }
306
  = let x = (d, Leaf) in ref x (* BUG: ref (d, Leaf) *)
307

308 309 310
  let replace (m : ref rbt) k v
    requires { inv !m }
    ensures { inv !m /\
311
      default !m = default (old !m) /\
312 313
      forall k':key, v':value.
      mem !m k' v' <-> if k' = k then v' = v else mem (old !m) k' v' }
314 315
  = let (d, t) = !m in
    m := (d, add t k v)
316

317 318 319 320
  let lookup (m : ref rbt) k
    requires { inv !m }
    ensures { mem !m k result }
  = let (d, t) = !m in
321 322
    try find t k with Not_found -> d end

323
  (* the easy way: implements `remove` using `replace` *)
324 325 326
  let remove (m : ref rbt) k
    requires { inv !m }
    ensures { inv !m /\
327
      default !m = default (old !m) /\
328 329
      forall k':key, v':value.
      mem !m k' v' <-> if k' = k then v' = default !m else mem (old !m) k' v' }
330
  = replace m k (default !m)
331

332
end