Red-black trees
Red-black trees problem from the VACID-0 benchmarks
Authors: Jean-Christophe Filliâtre
Topics: Trees / Data Structures
Tools: Why3
References: The VACID-0 Benchmarks
see also the index (by topic, by tool, by reference, by year)
module RedBlackTree (* Red-black trees (data type) *) type key = int type value = int type color = Red | Black type tree = | Leaf | Node color tree key value tree (* occurrence of a key/value pair in a tree *) predicate memt (t : tree) (k : key) (v : value) = match t with | Leaf -> false | Node _ l k' v' r -> (k = k' /\ v = v') \/ memt l k v \/ memt r k v end 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' (* binary search tree *) use int.Int predicate lt_tree (x : key) (t : tree) = forall k : key. forall v : value. memt t k v -> k < x predicate gt_tree (x : key) (t : tree) = forall k : key. forall v : value. memt t k v -> x < k 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 predicate bst (t : tree) = match t with | Leaf -> true | Node _ l k _ r -> bst l /\ bst r /\ lt_tree k l /\ gt_tree k r end lemma bst_Leaf : bst Leaf 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)) (* [rbtree n t]: red black tree invariant [t] is a properly balanced red-black tree, i.e. it satisfies the following two invariants: - a red node has no red son - any path from the root to a leaf has exactly [n] black nodes *) predicate is_not_red (t : tree) = match t with | Node Red _ _ _ _ -> false | Leaf | Node Black _ _ _ _ -> true end predicate rbtree (n : int) (t : tree) = match t with | Leaf -> n = 0 | Node Red l _ _ r -> rbtree n l /\ rbtree n r /\ is_not_red l /\ is_not_red r | Node Black l _ _ r -> rbtree (n-1) l /\ rbtree (n-1) r end lemma rbtree_Leaf: rbtree 0 Leaf lemma rbtree_Node1: forall k:key, v:value. rbtree 0 (Node Red Leaf k v Leaf) 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 (* lookup *) exception Not_found let rec find (t : tree) (k : key) : value requires { bst t } variant { t } ensures { memt t k result } raises { Not_found -> forall v : value. not (memt t k v) } = match t with | Leaf -> raise Not_found | Node _ l k' v r -> if k = k' then v else if k < k' then find l k else (* k > k' *) find r k end (* insertion *)
almost_rbtree n t
: t
may have one red-red conflict at its root;
it satisfies rbtree n
everywhere else
predicate almost_rbtree (n : int) (t : tree) = match t with | Leaf -> n = 0 | Node Red l _ _ r -> rbtree n l /\ rbtree n r | Node Black l _ _ r -> rbtree (n-1) l /\ rbtree (n-1) r end 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)
lbalance c x l r
acts as a black node constructor,
solving a possible red-red conflict on l
, using the following
schema:
B (R (R a x b) y c) z d 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
The result is not necessarily a black node.
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 | Node Red (Node Red a kx vx b) ky vy c | Node Red a kx vx (Node Red b ky vy c) -> Node Red (Node Black a kx vx b) ky vy (Node Black c k v r) | _ -> Node Black l k v r end
rbalance l x r
is similar to lbalance
, solving a possible red-red
conflict on r
. The balancing schema is similar:
B a x (R (R b y c) z d) 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
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 | Node Red (Node Red b ky vy c) kz vz d | Node Red b ky vy (Node Red c kz vz d) -> Node Red (Node Black l k v b) ky vy (Node Black c kz vz d) | _ -> Node Black l k v r end (* `insert x s` inserts `x` in tree `s`, resulting in a possible top red-red conflict when `s` is red. *) let rec insert (t : tree) (k : key) (v : value) : tree requires { bst t /\ exists n: int. rbtree n t } variant { t } 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 | 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 (* finally `add x s` calls `insert` and recolors the root as black *) 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) /\ 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 insert t k v with | Node _ l k' v' r -> Node Black l k' v' r | Leaf -> absurd end end module Vacid0 (* the VACID-0 interface = mutable map with default value*) use ref.Ref use RedBlackTree type rbt = (value, tree) predicate inv (r : rbt) = let (_, t) = r in bst t /\ exists n : int. rbtree n t let function default (r : rbt) : value = let (d, _) = r in d predicate mem (r : rbt) (k : key) (v : value) = let (d, t) = r in memt t k v \/ (v = d /\ forall v':value. not (memt t k v')) let create (d : int) ensures { inv !result /\ default !result = d /\ forall k:key, v:value. mem !result k v <-> v = d } = let x = (d, Leaf) in ref x (* BUG: ref (d, Leaf) *) let replace (m : ref rbt) k v requires { inv !m } ensures { inv !m /\ default !m = default (old !m) /\ forall k':key, v':value. mem !m k' v' <-> if k' = k then v' = v else mem (old !m) k' v' } = let (d, t) = !m in m := (d, add t k v) let lookup (m : ref rbt) k requires { inv !m } ensures { mem !m k result } = let (d, t) = !m in try find t k with Not_found -> d end (* the easy way: implements `remove` using `replace` *) let remove (m : ref rbt) k requires { inv !m } ensures { inv !m /\ default !m = default (old !m) /\ forall k':key, v':value. mem !m k' v' <-> if k' = k then v' = default !m else mem (old !m) k' v' } = replace m k (default !m) end
download ZIP archive