Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 1f907d94 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

vacid-0: red black trees in progress

parent 16b804ca
(* Red-black trees *)
{
type key = int
type value = int
......@@ -8,12 +10,53 @@
type tree =
| Leaf
| Node color tree key value tree
logic memt (t : tree) (k : key) (v : value) =
match t with
| Leaf -> false
| Node _ l k' v' r -> (k = k' and v = v') or memt l k v or memt r k v
end
}
(* static RedBlackTree create(int defaultValue); *)
(* void replace(int key, int value); *)
(* void remove(int key); *)
(* int lookup(int key); *)
(* the VACID-0 interface = map + default value *)
{
type rbt = (value, tree)
logic default (r : rbt) : value =
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 create d =
{ }
let x = (d, Leaf) in ref x (* BUG: ref (d, Leaf) *)
{ default !result = d and
forall k:key, v:value. mem !result k v <-> v = d }
parameter replace :
m:ref rbt -> k:key -> v:value ->
{}
unit writes m
{ 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' }
parameter lookup :
m:ref rbt -> k:key ->
{}
value reads m
{ mem !m k result }
(* the easy way (remove implemented using replace) *)
let remove m k =
{ }
replace m k (default !m)
{ default !m = default (old !m) and
forall k':key, v':value.
mem !m k' v' <-> if k' = k then v' = default !m else mem (old !m) k' v' }
(*
Local Variables:
......
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