stdlib/hashtbl.mlw

   1
   2 (** {1 Hash tables}
   3
   4   This module provides Hash tables à la OCaml.
   5   Each key is mapped to a {h <b>stack</b>} of values,
   6   with `add h k v` pushing a new value `v` for key `k`,
   7   and `remove h k` popping a value for key `k`.
   8
   9   For a simpler model of imperative finite maps,
  10   see modules `fmap.FmapImp` and `fmap.FmapImpInt`.
  11
  12 *)
  13
  14 module Hashtbl
  15
  16   use list.List
  17   use map.Map
  18
  19   type key
  20
  21   type t 'a = abstract { mutable contents: map key (list 'a) }
  22
  23   function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
  24
  25   val create (_n:int) : t 'a ensures { forall k: key. result[k] = Nil }
  26
  27   val clear (h: t 'a) : unit writes {h} ensures { forall k: key. h[k] = Nil }
  28
  29   val add (h: t 'a) (k: key) (v: 'a) : unit writes {h}
  30     ensures { h[k] = Cons v (old h)[k] }
  31     ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
  32
  33   val mem (h: t 'a) (k: key) : bool
  34     ensures { result=True <-> h[k] <> Nil }
  35
  36   val find (h: t 'a) (k: key) : 'a
  37     requires { h[k] <> Nil }
  38     ensures  { match h[k] with Nil -> false | Cons v _ -> result = v end }
  39
  40   val find_all (h: t 'a) (k: key) : list 'a
  41     ensures { result = h[k] }
  42
  43   exception NotFound
  44
  45   val defensive_find (h: t 'a) (k: key) : 'a
  46     ensures { match h[k] with Nil -> false | Cons v _ -> result = v end }
  47     raises  { NotFound -> h[k] = Nil }
  48
  49   val copy (h: t 'a) : t 'a
  50     ensures { forall k: key. result[k] = h[k] }
  51
  52   val remove (h: t 'a) (k: key) : unit writes {h}
  53     ensures { h[k] = match (old h)[k] with Nil -> Nil | Cons _ l -> l end }
  54     ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
  55
  56   val replace (h: t 'a) (k: key) (v: 'a) : unit writes {h}
  57     ensures {
  58       h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end) }
  59     ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
  60
  61   (*** TODO
  62      - val length: t 'a -> int (the number of distinct key)
  63      - val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
  64      - val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
  65   *)
  66
  67 end