vacid-0: red black trees in progress

parent 1f907d94
......@@ -18,7 +18,22 @@
end
}
(* the VACID-0 interface = map + default value *)
exception Not_found
parameter find :
t : tree -> k : key ->
{ }
value
{ memt t k result } | Not_found -> { forall v : value. not (memt t k v) }
parameter add :
t : tree -> k : key -> v : value ->
{}
tree
{ forall k':key, v':value.
memt result k' v' <-> if k' = k then v' = v else memt t k' v' }
(* the VACID-0 interface = mutable map with default value*)
{
type rbt = (value, tree)
......@@ -27,7 +42,8 @@
let (d, _) = r in d
logic mem (r : rbt) (k : key) (v : value) =
let (d, t) = r in memt t k v or v = d
let (d, t) = r in
memt t k v or (v = d and forall v':value. not (memt t k v'))
}
let create d =
......@@ -36,10 +52,10 @@ let create d =
{ default !result = d and
forall k:key, v:value. mem !result k v <-> v = d }
parameter replace :
m:ref rbt -> k:key -> v:value ->
let replace m k v =
{}
unit writes m
let (d, t) = !m in
m := (d, add t k v)
{ default !m = default (old !m) and
forall k':key, v':value.
mem !m k' v' <-> if k' = k then v' = v else mem (old !m) k' v' }
......@@ -50,7 +66,7 @@ parameter lookup :
value reads m
{ mem !m k result }
(* the easy way (remove implemented using replace) *)
(* the easy way (implements "remove" using "replace") *)
let remove m k =
{ }
replace m k (default !m)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment