Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

hashtbl.mlw 3.98 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 17 18
module Hashtbl

  use import list.List
  use import map.Map

  type key

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
21
  val create (n:int) :
22 23
    {} t 'a { forall k: key. result[k] = Nil }

Andrei Paskevich's avatar
Andrei Paskevich committed
24
  val clear (h: t 'a) :
25 26
    {} unit writes h { forall k: key. h[k] = Nil }

Andrei Paskevich's avatar
Andrei Paskevich committed
27
  val add (h: t 'a) (k: key) (v: 'a) :
28 29
    {}
    unit writes h
Andrei Paskevich's avatar
Andrei Paskevich committed
30
    { h[k] = Cons v (old h)[k] /\
31 32
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

Andrei Paskevich's avatar
Andrei Paskevich committed
33
  val mem (h: t 'a) (k: key) :
34 35 36
    {}
    bool reads h
    { result=True <-> h[k] <> Nil }
37

Andrei Paskevich's avatar
Andrei Paskevich committed
38
  val find (h: t 'a) (k: key) :
39 40 41
    { h[k] <> Nil }
    'a reads h
    { match h[k] with Nil -> false | Cons v _ -> result = v end }
42

Andrei Paskevich's avatar
Andrei Paskevich committed
43
  val find_all (h: t 'a) (k: key) :
44 45 46
    {}
    list 'a reads h
    { result = h[k] }
47

48
  exception NotFound
49

Andrei Paskevich's avatar
Andrei Paskevich committed
50
  val defensive_find (h: t 'a) (k: key) :
51 52 53 54
    {}
    'a reads h raises NotFound
    { match h[k] with Nil -> false | Cons v _ -> result = v end }
    | NotFound -> { h[k] = Nil }
55

Andrei Paskevich's avatar
Andrei Paskevich committed
56
  val copy (h: t 'a) :
57 58 59
    {}
    t 'a reads h
    { forall k: key. result[k] = h[k] }
60

Andrei Paskevich's avatar
Andrei Paskevich committed
61
  val remove (h: t 'a) (k: key) :
62
    {}
63
    unit writes h
64
    { h[k] = match (old h)[k] with Nil -> Nil | Cons _ l -> l end /\
65 66
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

Andrei Paskevich's avatar
Andrei Paskevich committed
67
  val replace (h: t 'a) (k: key) (v: 'a) :
68 69 70
    {}
    unit writes h
    { (h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end))
Andrei Paskevich's avatar
Andrei Paskevich committed
71
      /\
72 73
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

MARCHE Claude's avatar
MARCHE Claude committed
74
  (*** TODO
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75
     - val length: t 'a -> int (the number of distinct key)
76 77 78 79 80 81 82 83 84 85 86 87
     - 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

Andrei Paskevich's avatar
Andrei Paskevich committed
88 89 90 91
  function k1: key
  function k2: key
  function k3: key
  axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3
92 93 94 95 96 97 98 99 100 101 102 103

  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) }
104 105 106

end

107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
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

  type t 'a = {| mutable size: int; (* total number of elements *)
                 mutable data: array (list (key, 'a)); |}
    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)))

  let create (n:int) : t 'a =
    { 1 <= n }
    {| size = 0; data = Array.make n Nil |}
    { forall k: key. result[k] = Nil }

  let clear (h: t 'a) =
    {}
    h.size <- 0;
    Array.fill h.data 0 (Array.length h.data) Nil
    { forall k: key. h[k] = 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)

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

end