examples/vacid_0_red_black_trees.mlw

   1
   2 module RedBlackTree
   3
   4   (* Red-black trees (data type) *)
   5
   6   type key = int
   7   type value = int
   8
   9   type color = Red | Black
  10
  11   type tree =
  12     | Leaf
  13     | Node color tree key value tree
  14
  15   (* occurrence of a key/value pair in a tree *)
  16
  17   predicate memt (t : tree) (k : key) (v : value) =
  18     match t with
  19     | Leaf -> false
  20     | Node _ l k' v' r -> (k = k' /\ v = v') \/ memt l k v \/ memt r k v
  21     end
  22
  23   lemma memt_color :
  24     forall l r : tree, k k' : key, v v' : value, c c' : color.
  25     memt (Node c l k v r) k' v' -> memt (Node c' l k v r) k' v'
  26
  27   (* binary search tree *)
  28
  29   use int.Int
  30
  31   predicate lt_tree (x : key) (t : tree) =
  32     forall k : key. forall v : value. memt t k v -> k < x
  33
  34   predicate gt_tree (x : key) (t : tree) =
  35     forall k : key. forall v : value. memt t k v -> x < k
  36
  37   lemma lt_leaf: forall x: key. lt_tree x Leaf
  38
  39   lemma gt_leaf: forall x: key. gt_tree x Leaf
  40
  41   lemma lt_tree_node:
  42     forall x y: key, v: value, l r: tree, c: color.
  43     lt_tree x l -> lt_tree x r -> y < x -> lt_tree x (Node c l y v r)
  44
  45   lemma gt_tree_node:
  46     forall x y: key, v: value, l r: tree, c: color.
  47     gt_tree x l -> gt_tree x r -> x < y -> gt_tree x (Node c l y v r)
  48
  49   lemma lt_node_lt:
  50     forall x y: key, v: value, l r: tree, c: color.
  51     lt_tree x (Node c l y v r) -> y < x
  52
  53   lemma gt_node_gt:
  54     forall x y: key, v: value, l r: tree, c: color.
  55     gt_tree x (Node c l y v r) -> x < y
  56
  57   lemma lt_left:
  58     forall x y: key, v: value, l r: tree, c : color.
  59     lt_tree x (Node c l y v r) -> lt_tree x l
  60
  61   lemma lt_right:
  62     forall x y: key, v: value,  l r: tree, c: color.
  63     lt_tree x (Node c l y v r) -> lt_tree x r
  64
  65   lemma gt_left:
  66     forall x y: key, v: value, l r: tree, c: color.
  67     gt_tree x (Node c l y v r) -> gt_tree x l
  68
  69   lemma gt_right:
  70     forall x y: key, v: value, l r: tree, c: color.
  71     gt_tree x (Node c l y v r) -> gt_tree x r
  72
  73   lemma lt_tree_not_in:
  74     forall x: key, t: tree. lt_tree x t -> forall v: value. not (memt t x v)
  75
  76   lemma lt_tree_trans:
  77     forall x y: key. x < y -> forall t: tree. lt_tree x t -> lt_tree y t
  78
  79   lemma gt_tree_not_in :
  80     forall x: key, t: tree. gt_tree x t -> forall v: value. not (memt t x v)
  81
  82   lemma gt_tree_trans :
  83     forall x y: key. y < x -> forall t: tree. gt_tree x t -> gt_tree y t
  84
  85   predicate bst (t : tree) =
  86     match t with
  87     | Leaf -> true
  88     | Node _ l k _ r -> bst l /\ bst r /\ lt_tree k l /\ gt_tree k r
  89     end
  90
  91   lemma bst_Leaf : bst Leaf
  92
  93   lemma bst_left:
  94     forall k: key, v: value, l r: tree, c: color. bst (Node c l k v r) -> bst l
  95
  96   lemma bst_right:
  97     forall k: key, v: value, l r: tree, c: color. bst (Node c l k v r) -> bst r
  98
  99   lemma bst_color:
 100     forall c c': color, k: key, v: value, l r: tree.
 101     bst (Node c l k v r) -> bst (Node c' l k v r)
 102
 103   lemma rotate_left:
 104     forall kx ky: key, vx vy: value, a b c: tree, c1 c2 c3 c4: color.
 105     bst (Node c1 a kx vx (Node c2 b ky vy c)) ->
 106     bst (Node c3 (Node c4 a kx vx b) ky vy c)
 107
 108   lemma rotate_right:
 109     forall kx ky: key, vx vy: value, a b c: tree, c1 c2 c3 c4: color.
 110     bst (Node c3 (Node c4 a kx vx b) ky vy c) ->
 111     bst (Node c1 a kx vx (Node c2 b ky vy c))
 112
 113   (* [rbtree n t]: red black tree invariant
 114      [t] is a properly balanced red-black tree, i.e. it
 115       satisfies the following two invariants:
 116       - 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     match t with
 122     | Node Red _ _ _ _ -> false
 123     | Leaf | Node Black _ _ _ _ -> true
 124     end
 125
 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     end
 135
 136   lemma rbtree_Leaf:
 137     rbtree 0 Leaf
 138
 139   lemma rbtree_Node1:
 140     forall k:key, v:value. rbtree 0 (Node Red Leaf k v Leaf)
 141
 142   lemma rbtree_left:
 143     forall x: key, v: value, l r: tree, c: color.
 144     (exists n: int. rbtree n (Node c l x v r)) -> exists n: int. rbtree n l
 145
 146   lemma rbtree_right:
 147     forall x: key, v: value, l r: tree, c: color.
 148     (exists n: int. rbtree n (Node c l x v r)) -> exists n: int. rbtree n r
 149
 150   (* lookup *)
 151
 152   exception Not_found
 153
 154   let rec find (t : tree) (k : key) : value
 155     requires { bst t }
 156     variant { t }
 157     ensures { memt t k result }
 158     raises { Not_found -> forall v : value. not (memt t k v) }
 159   = match t with
 160     | Leaf -> raise Not_found
 161     | Node _ l k' v r ->
 162         if k = k' then v
 163         else if k < k' then find l k
 164         else (* k > k' *) find r k
 165     end
 166
 167   (* insertion *)
 168
 169   (** `almost_rbtree n t`: `t` may have one red-red conflict at its root;
 170       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   lemma rbtree_almost_rbtree:
 183     forall n: int, t: tree. rbtree n t -> almost_rbtree n t
 184
 185   lemma rbtree_almost_rbtree_ex:
 186     forall s: tree.
 187     (exists n: int. rbtree n s) -> exists n: int. almost_rbtree n s
 188
 189   lemma almost_rbtree_rbtree_black:
 190     forall x: key, v: value, l r: tree, n: int.
 191     almost_rbtree n (Node Black l x v r) -> rbtree n (Node Black l x v r)
 192
 193   (** `lbalance c x l r` acts as a black node constructor,
 194       solving a possible red-red conflict on `l`, using the following
 195       schema:
 196
 197       B (R (R a x b) y c) z d
 198       B (R a x (R b y c)) z d -> R (B a x b) y (R c z d)
 199       B a x b -> B a x b
 200
 201       The result is not necessarily a black node. *)
 202
 203   let lbalance (l : tree) (k : key) (v : value) (r : tree)
 204     requires { lt_tree k l /\ gt_tree k r /\ bst l /\ bst r }
 205     ensures { bst result /\
 206       (forall n : int. almost_rbtree n l -> rbtree n r -> rbtree (n+1) result)
 207       /\
 208       forall k':key, v':value.
 209         memt result k' v' <->
 210         if k' = k then v' = v else (memt l k' v' \/ memt r k' v') }
 211   = 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   (** `rbalance l x r` is similar to `lbalance`, solving a possible red-red
 220       conflict on `r`. The balancing schema is similar:
 221
 222       B a x (R (R b y c) z d)
 223       B a x (R b y (R c z d)) -> R (B a x b) y (R c z d)
 224       B a x b -> B a x b
 225    *)
 226
 227   let rbalance (l : tree) (k : key) (v : value) (r : tree)
 228     requires { lt_tree k l /\ gt_tree k r /\ bst l /\ bst r }
 229     ensures { bst result /\
 230       (forall n : int. almost_rbtree n r -> rbtree n l -> rbtree (n+1) result)
 231       /\
 232       forall k':key, v':value.
 233         memt result k' v' <->
 234         if k' = k then v' = v else (memt l k' v' \/ memt r k' v') }
 235   = 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   (* `insert x s` inserts `x` in tree `s`, resulting in a possible top red-red
 244      conflict when `s` is red. *)
 245
 246   let rec insert (t : tree) (k : key) (v : value) : tree
 247     requires { bst t /\ exists n: int. rbtree n t }
 248     variant { t }
 249     ensures { bst result /\
 250       (forall n : int. rbtree n t -> almost_rbtree n result /\
 251          (is_not_red t -> rbtree n result)) /\
 252       memt result k v /\
 253       forall k':key, v':value.
 254       memt result k' v' <-> if k' = k then v' = v else memt t k' v' }
 255   = match t with
 256     | Leaf ->
 257         Node Red Leaf k v Leaf
 258     | Node Red l k' v' r ->
 259         if k < k' then Node Red (insert l k v) k' v' r
 260         else if k' < k then Node Red l k' v' (insert r k v)
 261         else (* k = k' *) Node Red l k' v r
 262     | Node Black l k' v' r ->
 263         if k < k' then lbalance (insert l k v) k' v' r
 264         else if k' < k then rbalance l k' v' (insert r k v)
 265         else (* k = k' *) Node Black l k' v r
 266     end
 267
 268   (* finally `add x s` calls `insert` and recolors the root as black *)
 269
 270   let add (t : tree) (k : key) (v : value) : tree
 271     requires { bst t /\ exists n:int. rbtree n t }
 272     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   = match insert t k v with
 277     | Node _ l k' v' r -> Node Black l k' v' r
 278     | Leaf -> absurd
 279     end
 280
 281 end
 282
 283 module Vacid0
 284
 285   (* the VACID-0 interface = mutable map with default value*)
 286
 287   use ref.Ref
 288   use RedBlackTree
 289
 290   type rbt = (value, tree)
 291
 292   predicate inv (r : rbt) =
 293     let (_, t) = r in bst t /\ exists n : int. rbtree n t
 294
 295   let function default (r : rbt) : value =
 296     let (d, _) = r in d
 297
 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   let create (d : int)
 303     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   let replace (m : ref rbt) k v
 309     requires { inv !m }
 310     ensures { inv !m /\
 311       default !m = default (old !m) /\
 312       forall k':key, v':value.
 313       mem !m k' v' <-> if k' = k then v' = v else mem (old !m) k' v' }
 314   = let (d, t) = !m in
 315     m := (d, add t k v)
 316
 317   let lookup (m : ref rbt) k
 318     requires { inv !m }
 319     ensures { mem !m k result }
 320   = let (d, t) = !m in
 321     try find t k with Not_found -> d end
 322
 323   (* the easy way: implements `remove` using `replace` *)
 324   let remove (m : ref rbt) k
 325     requires { inv !m }
 326     ensures { inv !m /\
 327       default !m = default (old !m) /\
 328       forall k':key, v':value.
 329       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