vacid-0: red black trees (harness done)

examples/programs/vacid_0_red_black_trees.mlw

+
+{
+  type key = int
+  type value = int
+
+  type color = Red | Black
+
+  type tree =
+    | Leaf 
+    | Node color tree key value tree
+}
+
+(* static RedBlackTree create(int defaultValue); *)
+(* void replace(int key, int value); *)
+(* void remove(int key); *)
+(* int lookup(int key); *)
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_red_black_trees"
+End: 
+*)

examples/programs/vacid_0_red_black_trees_harness.mlw

+
+{
+  type key = int
+  type value = int
+  type rbt
+  logic default rbt : value
+  logic mem rbt key value
+}
+
+parameter create : 
+  d:value -> 
+  {} 
+  ref rbt 
+  { 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 }
+
+parameter remove :
+  m:ref rbt -> k:key -> 
+  {} 
+  unit writes 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' }
+
+let harness () =
+  let a = create 0 in
+  let b = create 1 in
+  replace a 1 1; replace b 1 10;
+  replace a 2 2; replace b 2 20;
+  let a1  = lookup a 1  in assert { a1  = 1  };
+  let a42 = lookup a 42 in assert { a42 = 0  };
+  let b1  = lookup b 1  in assert { b1  = 10 };
+  let b42 = lookup b 42 in assert { b42 = 1  };
+  remove a 1; remove b 2;
+  let a1  = lookup a 1  in assert { a1  = 0 };
+  let a42 = lookup a 42 in assert { a42 = 0 };
+  let b2  = lookup b 2  in assert { b2  = 1 };
+  let b42 = lookup b 42 in assert { b42 = 1 };
+  ()
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_red_black_trees_harness"
+End: 
+*)