examples/tests/hashtbl-test.mlw

   1 module TestHashtbl
   2
   3   use int.Int
   4   use list.List
   5   use hashtbl.Hashtbl
   6
   7   val constant k1: key
   8   val constant k2: key
   9   val constant k3: key
  10   axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3
  11
  12   let test1 () =
  13     let h = create 17 in
  14     add h k1 True;
  15     assert { h[k1] = Cons True Nil };
  16     assert { h[k2] = Nil };
  17     let v1 = find h k1 in
  18     assert { v1 = True };
  19     add h k1 False;
  20     assert { h[k1] = Cons False (Cons True Nil) };
  21     replace h k1 True;
  22     assert { h[k1] = Cons True (Cons True Nil) }
  23
  24 end
  25
  26