examples_in_progress/vacid_0_red_black_trees_harness.mlw

   1 module M
   2
   3   use ref.Ref
   4
   5   type key = int
   6   type value = int
   7   type rbt
   8   function default rbt : value
   9   predicate mem rbt key value
  10
  11   val create (d:value) : ref rbt
  12     ensures { default !result = d /\
  13       forall k:key, v:value. mem !result k v <-> v = d }
  14
  15   val replace (m:ref rbt) (k:key) (v:value) : unit writes {m}
  16     ensures { default !m = default (old !m) /\
  17       forall k':key, v':value.
  18       mem !m k' v' <-> if k' = k then v' = v else mem (old !m) k' v' }
  19
  20   val lookup (m:ref rbt) (k:key) : value
  21     ensures { mem !m k result }
  22
  23   val remove (m:ref rbt) (k:key) : unit writes {m}
  24     ensures { default !m = default (old !m) /\
  25       forall k':key, v':value.
  26       mem !m k' v' <-> if k' = k then v' = default !m else mem (old !m) k' v' }
  27
  28   let harness () =
  29     let a = create 0 in
  30     let b = create 1 in
  31     replace a 1 1; replace b 1 10;
  32     replace a 2 2; replace b 2 20;
  33     let a1  = lookup a 1  in assert { a1  = 1  };
  34     let a42 = lookup a 42 in assert { a42 = 0  };
  35     let b1  = lookup b 1  in assert { b1  = 10 };
  36     let b42 = lookup b 42 in assert { b42 = 1  };
  37     remove a 1; remove b 2;
  38     let a1  = lookup a 1  in assert { a1  = 0 };
  39     let a42 = lookup a 42 in assert { a42 = 0 };
  40     let b2  = lookup b 2  in assert { b2  = 1 };
  41     let b42 = lookup b 42 in assert { b42 = 1 };
  42     ()
  43
  44   end