Wiki Agenda Contact Version française

Hash tables with linear probing


Authors: Jean-Christophe Filliâtre / Martin Clochard

Topics: Array Data Structure / Data Structures

Tools: Why3

see also the index (by topic, by tool, by reference, by year)



Hash tables using linear probing

Authors: Jean-Christophe Filliâtre (CNRS) Martin Clochard (École Normale Supérieure)

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

module LinearProbing

  clone import HashedTypeWithDummy

  use import int.Int
  use import int.ComputerDivision
  use import option.Option
  use import list.Mem
  use import map.Map
  use map.Const
  use import ref.Ref
  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

j lies between l and r, cyclically

  predicate between (l j r: int) =
    l <= j < r || r < l <= j || j < r < l

number of dummy values in array a between l and u

  namespace NumOfDummy
    use int.NumOf

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

    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] }
      ensures  { numof a2 l u = numof a1 l u }
      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 }
      variant { n } ensures { numof a 0 n = n }
    = if n > 0 then dummy_const a (n-1)

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

  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 }

  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 *)

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

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

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

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

  let find (a: array key) (x: key) : int
    requires { neq x dummy }
    requires { let n = Array.length a in 0 < n /\ numofd a 0 n > 0 }
    ensures  { 0 <= result < Array.length a }
    ensures  { eq a[result] dummy || eq a[result] x }
    ensures  { forall j: int. 0 <= j < Array.length a ->
               between (bucket x (Array.length a)) j result ->
               neq a[j] x /\ neq a[j] dummy }
  =
    let n = Array.length a in
    let b = bucket x n in
    let rec find (i: int) : int
      requires { 0 <= i < n }
      requires { numofd a 0 n > 0 }
      requires { forall j: int. 0 <= j < n -> between b j i ->
                 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 }
      variant  { if i >= b then n - i + b else b - i }
      ensures  { 0 <= result < n }
      ensures  { eq a[result] dummy || eq a[result] x }
      ensures  { forall j: int. 0 <= j < n -> between b j result ->
                 neq a[j] x /\ neq a[j] dummy }
    =
      if eq a[i] dummy || eq a[i] x then i else find (next n i)
    in
    find b

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

  let resize (h: t) : unit
    writes  { h.data, h.loc }
    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
    let ghost l = ref (Const.const 0) in
    for i = 0 to n - 1 do
      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
                  if j < i then
                    let j2 = Map.get !l (keym x) in
                    0 <= j2 < n2 /\ eq a[j2] x /\
                    forall k: int. 0 <= k < n2 ->
                      between (bucket x n2) k j2 -> neq a[k] x /\ neq a[k] dummy
                  else
                    forall j2: int. 0 <= j2 < n2 -> neq a[j2] x }
      let x = h.data[i] in
      if neq x dummy then begin
        'L:
        let j = find a x in
        assert { eq a[j] dummy };
        a[j] <- x;
        assert { numofd a 0 (j+1) = numofd (at a 'L) 0 (j+1) - 1 };
        l := Map.set !l (keym x) j
      end
    done;
    h.loc <- !l;
    h.data <- a

  let add (h: t) (x: key) : unit
    requires { neq x dummy }
    writes   { h.size, h.data, h.data.elts, h.view, h.loc }
    ensures  { h.view = Map.set (old h.view) (keym x) True }
   =
    abstract
      ensures { h.size + 1 < Array.length h.data }
      if 2 * (h.size + 1) >= Array.length h.data then resize h
    end;
    let i = find h.data x in
    if eq h.data[i] dummy then begin
      'L:
      h.size <- h.size + 1;
      h.data[i] <- x;
      assert { numofd h.data 0 (i+1) =
               numofd (at h.data 'L) 0 (i+1) - 1 }
    end;
    ghost h.view <- Map.set h.view (keym x) True;
    ghost h.loc <- Map.set h.loc (keym x) i;
    ()

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

  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)

  (* 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)
                 (ghost f0: int) (j i: int) : unit
    requires { 0 <= f0 < Array.length a }
    requires { 0 <= j < Array.length a }
    requires { 0 <= i < Array.length a }
    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 }
    requires { not (Map.get view dummym) }
    requires { forall k: int. 0 <= k < Array.length a ->
               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) }
    variant  { if i >= f0 then Array.length a - i + f0 else f0 - i }
    ensures  { numofd a 0 (Array.length a) =
               numofd (old a) 0 (Array.length a) }
    ensures  { valid a view !loc }
   =
    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
        (* the hash index r lies cyclically between j and i *)
        delete a loc view f0 j i
      else begin
        let ghost a1 = Array.copy a in
        ghost NumOfDummy.numof_eq a a1 0 n;
        (* the hole j lies cyclically between hash index r and i *)
        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;
        a[i] <- dummy;
        ghost numof_update a a2 0 i n;
        delete a loc view f0 i i
      end
    end

  let remove (h: t) (x: key) : unit
    requires { neq x dummy }
    ensures  { h.view = Map.set (old h.view) (keym x) False }
  =
    let n = Array.length h.data in
    let j = find h.data x in
    if neq h.data[j] dummy then begin
      'L:
      h.data[j] <- dummy;
      assert { numofd h.data 0 (j+1) =
               numofd (at h.data 'L) 0 (j+1) + 1 };
      ghost h.view <- Map.set h.view (keym x) False;
      let l = ref h.loc in
      let f0 = find_dummy h.data j (next n j) in
      delete h.data l h.view f0 j j;
      ghost h.loc <- !l;
      h.size <- h.size - 1;
    end

end

download ZIP archive

Why3 Proof Results for Project "linear_probing"

Theory "linear_probing.HashedTypeWithDummy": fully verified in 0.01 s

ObligationsAlt-Ergo (0.99.1)
VC for neq0.01

Theory "linear_probing.LinearProbing": fully verified in 89.18 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Z3 (4.3.2)
bucket_bounds0.02---------
VC for numof_eq------------
split_goal_wp
  1. variant decrease0.01---------
2. precondition0.02---------
3. precondition0.02---------
4. postcondition---------0.06
5. postcondition---------0.04
VC for dummy_const------------
split_goal_wp
  1. variant decrease0.02---------
2. precondition0.02---------
3. precondition0.01---------
4. postcondition---------0.01
5. postcondition0.01---------
VC for numof_update------------
split_goal_wp
  1. assertion------------
split_goal_wp
  1. VC for numof_update0.06---------
2. VC for numof_update------0.04---
2. assertion------------
split_goal_wp
  1. VC for numof_update0.05---------
2. VC for numof_update------0.06---
3. postcondition---------0.36
VC for create------------
split_goal_wp
  1. array creation size0.02---------
2. type invariant0.02---------
3. type invariant---------0.02
4. type invariant0.02---------
5. postcondition0.02---------
VC for clear------------
split_goal_wp
  1. precondition0.01---------
2. type invariant0.02---------
3. type invariant---------0.02
4. type invariant0.04---------
5. type invariant0.02---------
6. postcondition0.02---------
7. postcondition0.02---------
VC for find------------
split_goal_wp
  1. index in array bounds0.03---------
2. postcondition0.02---------
3. postcondition0.04---------
4. postcondition0.02---------
5. index in array bounds0.01---------
6. postcondition0.01---------
7. postcondition0.02---------
8. postcondition0.02---------
9. variant decrease------------
split_goal_wp
  1. VC for find0.04---------
2. VC for find---------0.50
10. precondition0.02---------
11. precondition0.02---------
12. precondition0.06---------
13. precondition---------0.01
14. postcondition0.01---------
15. postcondition0.03---------
16. postcondition0.02---------
17. precondition0.02---------
18. precondition0.03---------
19. precondition0.02---------
20. precondition---------0.09
21. postcondition0.03---------
22. postcondition0.01---------
23. postcondition0.03---------
VC for mem------------
split_goal_wp
  1. precondition0.03---------
2. precondition0.02---------
3. index in array bounds0.02---------
4. postcondition---0.29------
VC for resize------------
split_goal_wp
  1. array creation size0.02---------
2. type invariant0.02---------
3. type invariant0.03---------
4. type invariant0.02---------
5. type invariant0.01---------
6. postcondition0.02---------
7. loop invariant init0.04---------
8. loop invariant init0.03---------
9. loop invariant init------------
split_goal_wp
  1. loop invariant init0.04---------
2. loop invariant init0.02---------
3. loop invariant init---------0.02
4. loop invariant init0.02---------
5. loop invariant init---------0.02
6. loop invariant init0.02---------
10. index in array bounds0.03---------
11. type invariant0.03---------
12. precondition0.02---------
13. precondition0.03---------
14. assertion---------0.14
15. index in array bounds0.03---------
16. assertion---------0.10
17. loop invariant preservation---------0.22
18. loop invariant preservation---0.09------
19. loop invariant preservation---0.26------
20. loop invariant preservation---------0.02
21. loop invariant preservation0.03---------
22. loop invariant preservation------------
split_goal_wp
  1. loop invariant preservation---------0.02
2. loop invariant preservation---------0.02
3. loop invariant preservation---------0.02
4. loop invariant preservation---------0.17
5. loop invariant preservation---------0.16
6. loop invariant preservation---------0.06
23. type invariant0.02---------
24. type invariant0.02---------
25. type invariant------------
split_goal_wp
  1. type invariant------------
inline_goal
  1. type invariant------------
split_goal_wp
  1. VC for resize0.02---0.030.01
2. VC for resize------0.08---
3. VC for resize------0.08---
4. VC for resize---------0.03
5. VC for resize---------0.02
6. VC for resize---------0.03
7. VC for resize0.77---0.10---
8. VC for resize------0.54---
26. type invariant0.03---------
27. postcondition0.02---------
VC for add------------
split_goal_wp
  1. VC for add0.01---------
2. VC for add0.02---------
3. precondition0.03------0.02
4. precondition0.02---------
5. index in array bounds0.02---------
6. index in array bounds0.02---------
7. assertion---------0.20
8. type invariant0.02---------
9. type invariant---------0.09
10. type invariant------------
inline_goal
  1. type invariant------------
split_goal_wp
  1. VC for add0.04---------
2. VC for add------1.690.65
3. VC for add---------0.99
4. VC for add---------0.28
5. VC for add---------0.21
6. VC for add---------0.76
7. VC for add------1.27---
8. VC for add---------0.94
11. type invariant0.02---------
12. postcondition0.04---------
13. type invariant0.02---------
14. type invariant---------0.09
15. type invariant---------0.26
16. postcondition0.04---------
VC for copy------------
split_goal_wp
  1. type invariant---------0.02
2. type invariant------------
3. type invariant---------1.26
VC for find_dummy------------
split_goal_wp
  1. index in array bounds0.02---------
2. postcondition0.02---------
3. postcondition0.02---------
4. postcondition0.03---------
5. postcondition0.01---------
6. variant decrease0.08---------
7. precondition0.01---------
8. precondition0.03---------
9. precondition0.04---------
10. precondition------------
split_goal_wp
  1. VC for find_dummy0.40---------
2. VC for find_dummy---0.05---0.03
11. precondition0.02---------
12. postcondition0.02---------
13. postcondition0.02---------
14. postcondition0.02---------
15. postcondition0.03---------
VC for delete------------
split_goal_wp
  1. index in array bounds0.02------0.01
2. variant decrease------------
split_goal_wp
  1. VC for delete0.02---------
2. VC for delete0.07---------
3. precondition0.02------0.01
4. precondition0.03------0.01
5. precondition0.02------0.01
6. precondition0.03---------
7. precondition---------0.02
8. precondition0.04---------
9. precondition0.06---------
10. precondition------------
inline_goal
  1. precondition0.36---------
11. precondition0.02---------
12. precondition0.02------0.01
13. precondition------------
split_goal_wp
  1. precondition---------0.02
2. precondition---------0.02
3. precondition0.01---------
4. precondition0.14---------
5. precondition---------0.02
14. postcondition0.10---------
15. postcondition0.02---------
16. precondition0.06---------
17. precondition0.03------0.01
18. index in array bounds0.02------0.02
19. precondition0.04---------
20. precondition------------
split_goal_wp
  1. precondition------0.05---
21. precondition0.06---------
22. precondition0.05---------
23. precondition0.04---------
24. index in array bounds0.03------0.02
25. precondition0.06---------
26. precondition------------
split_goal_wp
  1. precondition------0.07---
27. precondition---------0.09
28. variant decrease------------
split_goal_wp
  1. VC for delete0.12---------
2. VC for delete---------0.18
29. precondition0.03------0.01
30. precondition0.02------0.01
31. precondition0.02------0.01
32. precondition0.04---------
33. precondition0.07---------
34. precondition0.08---------
35. precondition0.06---------
36. precondition---0.200.79---
37. precondition0.03---------
38. precondition------------
split_goal_wp
  1. precondition------0.74---
2. precondition------0.57---
39. precondition------------
split_goal_wp
  1. precondition---0.10------
2. precondition---------0.73
3. precondition---0.18------
4. precondition---2.44------
5. precondition---2.28---1.14
40. postcondition0.03---------
41. postcondition0.10---------
42. postcondition------------
inline_goal
  1. postcondition------------
split_goal_wp
  1. VC for delete0.03---------
2. VC for delete0.06---------
3. VC for delete0.06---------
4. VC for delete0.04---------
5. VC for delete0.04---------
6. VC for delete0.06---------
7. VC for delete0.18---------
8. VC for delete---------0.14
VC for remove------------
split_goal_wp
  1. precondition0.02---------
2. precondition0.01---------
3. index in array bounds0.02---------
4. index in array bounds0.02---------
5. assertion---31.91---16.68
6. type invariant0.03---------
7. precondition0.02---------
8. precondition0.04---------
9. precondition0.04---------
10. precondition------------
split_goal_wp
  1. VC for remove---------0.26
2. VC for remove------0.07---
11. precondition0.13---------
12. precondition0.03---------
13. precondition0.04---------
14. precondition0.02---------
15. precondition0.03---------
16. precondition0.02---------
17. precondition0.03---------
18. precondition0.02---------
19. precondition0.04---------
20. precondition0.02---------
21. precondition------1.620.70
22. precondition4.01------1.11
23. type invariant---------0.12
24. type invariant---------0.17
25. type invariant------------
split_goal_wp
  1. type invariant0.02---------
26. type invariant0.02------0.01
27. postcondition0.03------0.00
28. postcondition---------3.34