linear_probing.mlw 11.2 KB
Newer Older
1

2 3
(** Hash tables using linear probing

4 5
    Authors: Jean-Christophe Filliâtre (CNRS)
             Martin Clochard (École Normale Supérieure)
6
*)
7

8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
module HashedTypeWithDummy

  use import int.Int

  type key
  type keym (** the logic model of a key *)
  function keym key: keym
  predicate eq (x y: key) = keym x = keym y
  val eq (x y: key) : bool ensures { result <-> eq x y }
  predicate neq (x y: key) = keym x <> keym y
  let neq (x y: key) : bool ensures { result <-> neq x y } = not (eq x y)

  function hash key : int
  axiom hash_nonneg: forall k: key. 0 <= hash k
  axiom hash_eq: forall x y: key. eq x y -> hash x = hash y

  constant dummy: key
  constant dummym: keym = keym dummy

end

29 30
module LinearProbing

31 32
  clone import HashedTypeWithDummy

33 34 35 36 37
  use import int.Int
  use import int.ComputerDivision
  use import option.Option
  use import list.Mem
  use import map.Map
38
  use map.Const
39
  use import ref.Ref
40 41 42 43 44 45 46 47
  use import array.Array

  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

48
  (** j lies between l and r, cyclically *)
49
  predicate between (l j r: int) =
50
    l <= j < r || r < l <= j || j < r < l
51

52 53
  (** number of dummy values in array [a] between [l] and [u] *)
  namespace NumOfDummy
54 55 56 57
    use int.NumOf

    function numof (a: array key) (l u: int) : int =
      NumOf.numof (\ i. eq a[i] dummy) l u
58

59 60 61
    let rec lemma numof_eq (a1 a2: array key) (l u: int) : unit
      requires { 0 <= l <= u <= length a1 = length a2 }
      requires { forall i: int. l <= i < u -> eq a2[i] a1[i] }
62
      ensures  { numof a2 l u = numof a1 l u }
63 64 65 66 67
      variant  { u-l }
    = if l < u then numof_eq a1 a2 (l+1) u

    let rec lemma dummy_const (a: array key) (n: int)
      requires { 0 <= n } requires { forall i: int. 0 <= i < n -> a[i] = dummy }
68
      variant { n } ensures { numof a 0 n = n }
69
    = if n > 0 then dummy_const a (n-1)
70

71
  end
72
  function numofd (a: array key) (l u: int) : int = NumOfDummy.numof a l u
73

74 75 76 77 78 79 80 81 82 83 84 85 86
  let ghost numof_update (a1 a2: array key) (l i u: int)
    requires { 0 <= l <= i < u <= Array.length a1 = Array.length a2 }
    requires { forall j: int. l <= j < u -> j<>i -> a1[j] = a2[j] }
    requires { eq a1[i] dummy && neq a2[i] dummy }
    ensures  { numofd a1 l u = 1 + numofd a2 l u }
  =
     assert { numofd a1 l u
              = numofd a1 l i + numofd a1 i u
              = numofd a1 l i + numofd a1 i (i+1) + numofd a1 (i+1) u };
     assert { numofd a2 l u
              = numofd a2 l i + numofd a2 i u
              = numofd a2 l i + numofd a2 i (i+1) + numofd a2 (i+1) u }

87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
  predicate valid (data: array key) (view: map keym bool) (loc : map keym int) =
    (* dummy not in the model *)
    not (Map.get view dummym)
    /\
    (* any value in the array is in the model *)
    (forall i: int. 0 <= i < Array.length data ->
       let x = data[i] in neq x dummy ->
       Map.get view (keym x) /\ Map.get loc (keym x) = i)
    /\
    (* any value in the model is in the array *)
    (let n = Array.length data in
     forall x: key. Map.get view (keym x) ->
        let i = Map.get loc (keym x) in
        0 <= i < n && eq data[i] x &&
        forall j: int. 0 <= j < n ->
          between (bucket x n) j i ->
          neq data[j] x /\ neq data[j] dummy)
          (* TODO ^^^^^^^^^^^^^^^^^^ is actually provable *)

106 107
  type t = { mutable size: int;   (* total number of elements *)
             mutable data: array key;    (* buckets *)
108 109
       ghost mutable view: map keym bool; (* pure model *)
       ghost mutable loc : map keym int;  (* index where it is stored *)
110 111 112 113
    }
    (* at least one empty slot *)
    invariant { 0 <= self.size < length self.data }
    invariant { let n = Array.length self.data in
114
                self.size + numofd self.data 0 n = n }
115
    invariant { valid self.data self.view self.loc }
116 117 118

  let create (n: int) : t
    requires { 0 < n }
119
    ensures  { forall x: key. not (Map.get result.view (keym x)) }
120
  =
121
    { size = 0; data = Array.make n dummy;
122
      view = Const.const false; loc = Const.const 0; }
123 124 125 126

  let clear (h: t) : unit
    writes  { h.size, h.data.elts, h.view }
    ensures { h.size = 0 }
127
    ensures { forall x: key. not (Map.get h.view (keym x)) }
128 129 130
  =
    h.size <- 0;
    Array.fill h.data 0 (Array.length h.data) dummy;
131
    h.view <- Const.const false
132 133 134 135

  function next (n i: int) : int =
    let i = i+1 in if i = n then 0 else i

136
  let find (a: array key) (x: key) : int
137 138
    requires { neq x dummy }
    requires { let n = Array.length a in 0 < n /\ numofd a 0 n > 0 }
139
    ensures  { 0 <= result < Array.length a }
140
    ensures  { eq a[result] dummy || eq a[result] x }
141 142
    ensures  { forall j: int. 0 <= j < Array.length a ->
               between (bucket x (Array.length a)) j result ->
143
               neq a[j] x /\ neq a[j] dummy }
144
  =
145
    let n = Array.length a in
146
    let b = bucket x n in
147 148
    let rec find (i: int) : int
      requires { 0 <= i < n }
149
      requires { numofd a 0 n > 0 }
150
      requires { forall j: int. 0 <= j < n -> between b j i ->
151 152 153
                 neq a[j] x /\ neq a[j] dummy }
      requires { if i >= b then numofd a b i = 0
                 else numofd a b n = numofd a 0 i = 0 }
154
      variant  { if i >= b then n - i + b else b - i }
155
      ensures  { 0 <= result < n }
156
      ensures  { eq a[result] dummy || eq a[result] x }
157
      ensures  { forall j: int. 0 <= j < n -> between b j result ->
158
                 neq a[j] x /\ neq a[j] dummy }
159
    =
160
      if eq a[i] dummy || eq a[i] x then i else find (next n i)
161
    in
162
    find b
163

164
  let mem (h: t) (x: key) : bool
165 166
    requires { neq x dummy }
    ensures  { result <-> Map.get h.view (keym x) }
167
   =
168
    neq h.data[find h.data x] dummy
169 170

  let resize (h: t) : unit
171
    writes  { h.data, h.loc }
172 173 174 175 176
    ensures { Array.length h.data = 2 * old (Array.length h.data) }
  =
    let n = Array.length h.data in
    let n2 = 2 * n in
    let a = Array.make n2 dummy in
177
    let ghost l = ref (Const.const 0) in
178
    for i = 0 to n - 1 do
179 180 181 182 183
      invariant { numofd a 0 n2 = numofd h.data 0 i + n2 - i }
      invariant { forall j: int. 0 <= j < n2 -> neq a[j] dummy ->
                  Map.get h.view (keym a[j]) /\ Map.get !l (keym a[j]) = j }
      invariant { forall x: key. Map.get h.view (keym x) ->
                  let j = Map.get h.loc (keym x) in
184
                  if j < i then
185 186
                    let j2 = Map.get !l (keym x) in
                    0 <= j2 < n2 /\ eq a[j2] x /\
187
                    forall k: int. 0 <= k < n2 ->
188
                      between (bucket x n2) k j2 -> neq a[k] x /\ neq a[k] dummy
189
                  else
190
                    forall j2: int. 0 <= j2 < n2 -> neq a[j2] x }
191
      let x = h.data[i] in
192
      if neq x dummy then begin
193 194
        'L:
        let j = find a x in
195
        assert { eq a[j] dummy };
196
        a[j] <- x;
197 198
        assert { numofd a 0 (j+1) = numofd (at a 'L) 0 (j+1) - 1 };
        l := Map.set !l (keym x) j
199
      end
200
    done;
201
    h.loc <- !l;
202 203 204
    h.data <- a

  let add (h: t) (x: key) : unit
205
    requires { neq x dummy }
206
    writes   { h.size, h.data, h.data.elts, h.view, h.loc }
207
    ensures  { h.view = Map.set (old h.view) (keym x) True }
208
   =
209 210 211 212
    abstract
      ensures { h.size + 1 < Array.length h.data }
      if 2 * (h.size + 1) >= Array.length h.data then resize h
    end;
213
    let i = find h.data x in
214
    if eq h.data[i] dummy then begin
215 216 217
      'L:
      h.size <- h.size + 1;
      h.data[i] <- x;
218 219
      assert { numofd h.data 0 (i+1) =
               numofd (at h.data 'L) 0 (i+1) - 1 }
220
    end;
221 222
    ghost h.view <- Map.set h.view (keym x) True;
    ghost h.loc <- Map.set h.loc (keym x) i;
223 224 225 226 227 228 229
    ()

  let copy (h: t) : t
    ensures { result.view = h.view }
   =
    { size = h.size; data = Array.copy h.data;
      view = h.view; loc = h.loc; }
230

231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
  let rec ghost find_dummy (a: array key) (s: int) (i: int) : int
    requires { 0 <= s < Array.length a }
    requires { 0 <= i < Array.length a }
    requires { i <> s }
    requires { if i >= s then numofd a i (Array.length a) + numofd a 0 s >= 1
                         else numofd a i s >= 1}
    requires { forall k: int. 0 <= k < Array.length a ->
               between s k i -> k<>s -> neq a[k] dummy }
    variant  { if i >= s then Array.length a - i + s else s - i}
    ensures  { 0 <= result < Array.length a }
    ensures  { result <> s }
    ensures  { eq a[result] dummy }
    ensures  { forall k: int. 0 <= k < Array.length a ->
               between s k result -> k<>s -> neq a[k] dummy }
  =
    let n = Array.length a in
    if eq a[i] dummy then i else find_dummy a s (next n i)

249 250 251 252 253
  (* j is the hole just created by remove (see below) and this function
     restores the data structure invariant for elements
     to the right of j if needed, starting at index i *)
  let rec delete (a: array key)
                 (ghost loc: ref (map keym int)) (ghost view: map keym bool)
254 255
                 (ghost f0: int) (j i: int) : unit
    requires { 0 <= f0 < Array.length a }
256 257
    requires { 0 <= j < Array.length a }
    requires { 0 <= i < Array.length a }
258 259 260 261 262 263
    requires { j <> f0 }
    requires { eq a[j] dummy }
    requires { eq a[f0] dummy }
    requires { between j i f0 }
    requires { forall k: int. 0 <= k < Array.length a ->
               between i k f0 -> k<>i -> neq a[k] dummy }
264
    requires { not (Map.get view dummym) }
265
    requires { forall k: int. 0 <= k < Array.length a ->
266 267 268 269 270 271 272 273 274 275 276
               let x = a[k] in neq x dummy ->
               Map.get view (keym x) /\ Map.get !loc (keym x) = k }
    (* any value in the model is in the array *)
    requires { let n = Array.length a in
               forall x: key. Map.get view (keym x) ->
                 let k = Map.get !loc (keym x) in
                 0 <= k < n && eq a[k] x &&
                 forall l: int. 0 <= l < n -> between (bucket x n) l k ->
                   neq a[l] x /\
                   (neq a[l] dummy \/
                    l = j /\ between j i k) }
277
    variant  { if i >= f0 then Array.length a - i + f0 else f0 - i }
278 279
    ensures  { numofd a 0 (Array.length a) =
               numofd (old a) 0 (Array.length a) }
280
    ensures  { valid a view !loc }
281 282 283 284 285 286 287
   =
    let n = Array.length a in
    let i = next n i in
    let xi = a[i] in
    if neq xi dummy then begin
      let r = bucket xi n in
      if j < r && r <= i || i < j && j < r || r <= i && i < j then
288
        (* the hash index r lies cyclically between j and i *)
289
        delete a loc view f0 j i
290
      else begin
291 292
        let ghost a1 = Array.copy a in
        ghost NumOfDummy.numof_eq a a1 0 n;
293
        (* the hole j lies cyclically between hash index r and i *)
294 295 296 297 298
        a[j] <- xi;
        ghost numof_update a1 a 0 j n;
        let ghost a2 = Array.copy a in
        ghost NumOfDummy.numof_eq a a2 0 n;
        ghost loc := Map.set !loc (keym xi) j;
299
        a[i] <- dummy;
300 301
        ghost numof_update a a2 0 i n;
        delete a loc view f0 i i
302 303 304
      end
    end

305
  let remove (h: t) (x: key) : unit
306 307
    requires { neq x dummy }
    ensures  { h.view = Map.set (old h.view) (keym x) False }
308
  =
309
    let n = Array.length h.data in
310
    let j = find h.data x in
311
    if neq h.data[j] dummy then begin
312 313
      'L:
      h.data[j] <- dummy;
314
      assert { numofd h.data 0 (j+1) =
315 316
               numofd (at h.data 'L) 0 (j+1) + 1 };
      ghost h.view <- Map.set h.view (keym x) False;
317
      let l = ref h.loc in
318 319
      let f0 = find_dummy h.data j (next n j) in
      delete h.data l h.view f0 j j;
320
      ghost h.loc <- !l;
321 322 323
      h.size <- h.size - 1;
    end

324
end