hashtbl.mlw 4.01 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3
(** {1 Hash tables}

4
This module provides Hash tables à la OCaml. Each key is mapped to a {h <b>stack</b>} of values,
5
   with [add h k v] pushing a new value [v] for key [k],
6
   and [remove h k] popping a value for key [k].
MARCHE Claude's avatar
MARCHE Claude committed
7 8

*)
9

10 11 12 13 14 15 16
module Hashtbl

  use import list.List
  use import map.Map

  type key

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

Andrei Paskevich's avatar
Andrei Paskevich committed
19
  function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
20

21
  val create (n:int) : t 'a ensures { forall k: key. result[k] = Nil }
22

23
  val clear (h: t 'a) : unit writes {h} ensures { forall k: key. h[k] = Nil }
24

25 26 27
  val add (h: t 'a) (k: key) (v: 'a) : unit writes {h}
    ensures { h[k] = Cons v (old h)[k] }
    ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
28

29 30
  val mem (h: t 'a) (k: key) : bool reads {h}
    ensures { result=True <-> h[k] <> Nil }
31

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

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

39
  exception NotFound
40

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

45 46 47 48 49 50 51 52 53 54 55
  val copy (h: t 'a) : t 'a reads {h}
    ensures { forall k: key. result[k] = h[k] }

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

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

MARCHE Claude's avatar
MARCHE Claude committed
57
  (*** TODO
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
58
     - val length: t 'a -> int (the number of distinct key)
59 60 61 62 63 64 65 66 67 68
     - 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
69
  use import Hashtbl
70

Andrei Paskevich's avatar
Andrei Paskevich committed
71 72 73 74
  function k1: key
  function k2: key
  function k3: key
  axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3
75 76 77 78 79 80 81 82 83 84 85 86

  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) }
87 88 89

end

90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
module HashtblImpl

  use import int.Int
  use import int.ComputerDivision
  use import list.List
  use import list.Mem
  use import array.Array

  type key

  function hash key : int

  axiom hash_nonneg: forall k: key. 0 <= hash k

  function bucket (k: key) (n: int) : int = mod (hash k) n

  lemma bucket_bounds:
    forall n: int. 0 < n ->
    forall k: key. 0 <= bucket k n < n

110 111
  type t 'a = { mutable size: int; (* total number of elements *)
                 mutable data: array (list (key, 'a)); }
112 113 114 115 116 117 118 119 120 121 122 123 124
    invariant { let n = Array.length data in
                0 < n /\
                forall i: int. 0 <= i < n ->
                forall k: key, v: 'a. mem (k, v) data[i] -> bucket k n = i }

  function extract (k: key) (l: list (key, 'a)) : list 'a = match l with
    | Nil -> Nil
    | Cons (k', v) r -> if k = k' then Cons v (extract k r) else extract k r
  end

  function ([]) (t: t 'a) (k: key): list 'a =
    extract k (Array.get t.data (bucket k (length t.data)))

125 126 127 128
  let create (n:int) : t 'a
    requires { 1 <= n }
    ensures  { forall k: key. result[k] = Nil }
  = { size = 0; data = Array.make n Nil }
129

130 131 132
  let clear (h: t 'a)
    ensures { forall k: key. h[k] = Nil }
  = h.size <- 0;
133 134 135 136 137 138
    Array.fill h.data 0 (Array.length h.data) Nil

  lemma extract_neq:
    forall k k': key, v: 'a, l: list (key, 'a).
    k <> k' -> extract k' l = extract k' (Cons (k, v) l)

139 140
  let add (h: t 'a) (k: key) (v: 'a)
    ensures { h[k] = Cons v (old h)[k] /\
141
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }
142 143
  = let b = bucket k (Array.length h.data) in
    h.data[b] <- Cons (k, v) (Array.([]) h.data b)
144 145

end