hashtbl.mlw 2.37 KB
Newer Older
1 2 3 4 5 6 7 8 9 10

module Hashtbl

  use import list.List
  use import map.Map

  type key

  type t 'a model {| mutable contents: map key (list 'a) |}

11
  logic ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
12

13
  parameter create (n:int) :
14 15
    {} t 'a { forall k: key. result[k] = Nil }

16
  parameter clear (h: t 'a) :
17 18
    {} unit writes h { forall k: key. h[k] = Nil }

19
  parameter add (h: t 'a) (k: key) (v: 'a) :
20 21 22 23 24
    {}
    unit writes h
    { h[k] = Cons v (old h)[k] and
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

25 26 27 28
  parameter mem (h: t 'a) (k: key) :
    {}
    bool reads h
    { result=True <-> h[k] <> Nil }
29

30 31 32 33
  parameter find (h: t 'a) (k: key) :
    { h[k] <> Nil }
    'a reads h
    { match h[k] with Nil -> false | Cons v _ -> result = v end }
34

35 36 37 38
  parameter find_all (h: t 'a) (k: key) :
    {}
    list 'a reads h
    { result = h[k] }
39

40
  exception NotFound
41

42 43 44 45 46
  parameter defensive_find (h: t 'a) (k: key) :
    {}
    'a reads h raises NotFound
    { match h[k] with Nil -> false | Cons v _ -> result = v end }
    | NotFound -> { h[k] = Nil }
47

48 49 50 51
  parameter copy (h: t 'a) :
    {}
    t 'a reads h
    { forall k: key. result[k] = h[k] }
52

53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
  parameter remove (h: t 'a) (k: key) :
    { h[k] <> Nil }
    unit writes h
    { (match (old h)[k] with Nil -> false | Cons _ l -> h[k] =l end) and
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

  parameter replace (h: t 'a) (k: key) (v: 'a) :
    {}
    unit writes h
    { (h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end))
      and
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

  parameter length (h: t 'a) :
    {}
    int reads h
    {} (* = the number of distinct keys *)

  (* TODO
     - val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
     - val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
  *)

end

module TestHashtbl

  use import int.Int
  use import list.List
  use import module Hashtbl

  logic k1: key
  logic k2: key
  logic k3: key
  axiom kdiff : k1 <> k2 and k1 <> k3 and k2 <> k3

  let test1 () =
    let h = create 17 in
    add h k1 True;
    assert { h[k1] = Cons True Nil };
    assert { h[k2] = Nil };
    let v1 = find h k1 in
    assert { v1 = True };
    add h k1 False;
    assert { h[k1] = Cons False (Cons True Nil) };
    replace h k1 True;
    assert { h[k1] = Cons True (Cons True Nil) }
100 101 102 103 104 105 106 107 108


end

(*
Local Variables:
compile-command: "unset LANG; make -C .. modules/hashtbl"
End:
*)