hashtbl_impl.mlw 4.94 KB
Newer Older
1 2 3 4 5 6

(* Hash table implementation

   Jean-Christophe Filliâtre (CNRS)
   Andrei Paskevich (Univ Paris Sud) *)

7 8 9 10 11 12 13 14
module HashtblImpl

  use import int.Int
  use import int.ComputerDivision
  use import option.Option
  use import list.List
  use import list.Mem
  use import map.Map
15
  use import map.Const
16 17 18 19
  use import array.Array

  type key

20 21
  val eq (x y : key) : bool
    ensures { result <-> x = y }
22

23 24
  val function hash key : int
    ensures { 0 <= result }
25

26 27 28 29
  let function bucket (k: key) (n: int) : int
    requires { 0 < n }
    ensures { 0 <= result < n }
  = mod (hash k) n
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48

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

  predicate in_data (k: key) (v: 'a) (d: array (list (key, 'a))) =
    mem (k,v) d[bucket k (length d)]

  predicate good_data (k: key) (v: 'a)
      (m: map key (option 'a)) (d: array (list (key, 'a))) =
    Map.get m k = Some v <-> in_data k v d

  predicate good_hash (d: array (list (key, 'a))) (i: int) =
    forall k: key, v: 'a. mem (k,v) d[i] -> bucket k (length d) = i

  type t 'a = { mutable size: int;   (* total number of elements *)
                mutable data: array (list (key, 'a)); (* buckets *)
          ghost mutable view: map key (option 'a); (* pure model *) }

49
    invariant { 0 < length data }
50
    invariant {
51 52
      forall i: int. 0 <= i < length data -> good_hash data i }
    invariant { forall k: key, v: 'a. good_data k v view data }
53
    by { size = 0; data = make 1 Nil; view = Const.const None }
54 55 56

  let create (n: int) : t 'a
    requires { 1 <= n }
57
    ensures  { result.view = Const.const None }
58
  =
59
    { size = 0; data = make n Nil; view = Const.const None }
60 61 62

  let clear (h: t 'a) : unit
    writes  { h.size, h.data.elts, h.view }
63
    ensures { h.view = Const.const None }
64 65 66
  =
    h.size <- 0;
    fill h.data 0 (length h.data) Nil;
67
    h.view <- Const.const None
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87

  let resize (h: t 'a) : unit
    writes  { h.data }
  =
    let odata = h.data in
    let osize = length odata in
    let nsize = 2 * osize + 1 in
    let ndata = make nsize Nil in
    let rec rehash (ghost i : int) l
      requires { forall k: key, v: 'a. mem (k,v) l -> bucket k osize = i }
      requires { forall j: int. 0 <= j < nsize -> good_hash ndata j }
      requires { forall k: key, v: 'a.
        if 0 <= bucket k osize < i then good_data k v h.view ndata
        else if bucket k osize = i then
          (Map.get h.view k = Some v <-> mem (k,v) l \/ in_data k v ndata)
        else not in_data k v ndata }
      ensures  { forall j: int. 0 <= j < nsize -> good_hash ndata j }
      ensures  { forall k: key, v: 'a.
        if 0 <= bucket k osize <= i then good_data k v h.view ndata
        else not in_data k v ndata }
88
      variant  { l }
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
    = match l with
      | Nil -> ()
      | Cons (k, v) r ->
          let b = bucket k nsize in
          ndata[b] <- Cons (k, v) (ndata[b]);
          rehash i r
    end in
    for i = 0 to osize - 1 do
      invariant { forall j: int. 0 <= j < nsize -> good_hash ndata j }
      invariant { forall k: key, v: 'a.
        if 0 <= bucket k osize < i then good_data k v h.view ndata
        else not in_data k v ndata }
      rehash i odata[i]
    done;
    h.data <- ndata

105 106 107 108 109 110
  let rec list_find (k: key) (l: list (key, 'a)) : option 'a
    variant { l }
    ensures { match result with
              | None -> forall v: 'a. not (mem (k, v) l)
              | Some v -> mem (k, v) l
              end }
111
  = match l with
112
    | Nil -> None
113
    | Cons (k', v) r -> if eq k k' then Some v else list_find k r
114
    end
115

116
  let find (h: t 'a) (k: key) : option 'a
117
    ensures { result = Map.get h.view k }
118 119 120 121 122 123 124
  =
    let i = bucket k (length h.data) in
    list_find k h.data[i]

  let rec list_remove (k: key) (l: list (key, 'a)) : list (key, 'a)
    variant { l }
    ensures { forall k': key, v: 'a.
125 126
                mem (k',v) result <-> mem (k',v) l /\ k' <> k }
  = match l with
127 128
    | Nil -> Nil
    | Cons ((k', _) as p) r ->
129
        if eq k k' then list_remove k r else Cons p (list_remove k r)
130 131 132 133 134 135
    end

  let remove (h: t 'a) (k: key) : unit
    writes  { h.data.elts, h.view, h.size }
    ensures { Map.get h.view k = None }
    ensures { forall k': key. k' <> k ->
136 137
                Map.get h.view k' = Map.get (old h.view) k' }
  = let i = bucket k (length h.data) in
138 139 140 141 142 143 144 145 146 147 148
    let l = h.data[i] in
    match list_find k l with
    | None ->
        ()
    | Some _ ->
        h.data[i] <- list_remove k l;
        h.size <- h.size - 1;
        h.view <- Map.set h.view k None
    end

  let add (h: t 'a) (k: key) (v: 'a) : unit
149
    writes  { h, h.data.elts }
150 151
    ensures { Map.get h.view k = Some v }
    ensures { forall k': key. k' <> k ->
152
                Map.get h.view k' = Map.get (old h.view) k' }
153
  =
154
    if h.size = length h.data then resize h;
155 156 157 158 159 160
    remove h k;
    let i = bucket k (length h.data) in
    h.data[i] <- Cons (k, v) h.data[i];
    h.size <- h.size + 1;
    h.view <- Map.set h.view k (Some v)

161
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
162
  let alias (h: t int) (k: key) : unit =
163
    let old_data = h.data in
Andrei Paskevich's avatar
Andrei Paskevich committed
164
    add h k 42;
165 166 167
    old_data[0] <- Nil
*)
end