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 int.Int

  type key
  type keym

the logic model of a key

  function keym key: keym

  val predicate eq (x y: key)
    ensures { result <-> keym x = keym y }
  let predicate neq (x y: key)
    ensures { result <-> keym x <> keym y }
  = not (eq x y)

  val 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

  val constant dummy: key
  constant dummym: keym = keym dummy

end

module LinearProbing

  clone HashedTypeWithDummy with axiom .

  use int.Int
  use int.ComputerDivision
  use option.Option
  use list.Mem
  use map.Map
  use map.Const
  use ref.Ref
  use array.Array

  let function bucket (k: key) (n: int) : int
    requires { 0 < n }
    ensures { 0 <= result < n }
  = mod (hash k) n

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

j lies between l and r, cyclically

  scope NumOfDummy
    use int.NumOf

number of dummy values in array a between l and u

    function numof (a: array key) (l u: int) : int =
      NumOf.numof (fun 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 <= size < length data }
    invariant { let n = Array.length data in
                size + numofd data 0 n = n }
    invariant { valid data view 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

  let 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
        label L in
        let j = find a x in
        assert { eq a[j] dummy };
        a[j] <- x;
        assert { numofd a 0 (j+1) = numofd (a at 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 }
   =
    begin
      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
      label L in
      h.size <- h.size + 1;
      h.data[i] <- x;
      assert { numofd h.data 0 (i+1) =
               numofd (h.data at 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
      label L in
      h.data[j] <- dummy;
      assert { numofd h.data 0 (j+1) =
               numofd (h.data at 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

ObligationsAlt-Ergo 1.30
VC neq0.00
VC dummy0.00

Theory "linear_probing.LinearProbing": fully verified

ObligationsAlt-Ergo 1.30Alt-Ergo 2.0.0CVC3 2.4.1CVC4 1.4CVC4 1.5Z3 4.5.0Z3 4.6.0
VC bucket0.01------------------
NumOfDummy.VC numof_eq---------3.57---------
NumOfDummy.VC dummy_const0.10------------------
VC numof_update0.64------------------
VC t---------------------
exists 0
VC t.0---------------------
exists (make 1 dummy)
VC t.0.0---------------------
exists (fun (_:keym1) -> False)
VC t.0.0.0---------------------
exists (fun (_:keym1) -> 0)
VC t.0.0.0.0------------0.05------
VC create0.02------------------
VC clear0.07------------------
VC next0.01------------------
VC find---------------------
split_goal_right
VC find.00.01------------------
VC find.10.00------------------
VC find.20.01------------------
VC find.3---------------0.12---
VC find.40.01------------------
VC find.50.00------------------
VC find.60.04------------------
VC find.70.16------------------
VC find.80.01------------------
VC find.90.01------------------
VC find.100.01------------------
VC find.110.01------------------
VC find.120.01------------------
VC find.130.01------------------
VC find.140.01------------------
VC find.150.01------------------
VC find.160.00------------------
VC find.170.01------------------
VC mem---------1.59---------
VC resize---------------------
split_goal_right
VC resize.00.01------------------
VC resize.10.01------------------
VC resize.20.01------------------
VC resize.3---------------0.02---
VC resize.40.01------------------
VC resize.50.00------------------
VC resize.60.03------------------
VC resize.7---------2.03---0.03---
VC resize.80.01------------------
VC resize.9---------------0.38---
VC resize.10---------------0.21---
VC resize.11---------------3.50---
VC resize.12---------------------
split_goal_right
VC resize.12.0------0.76------------
VC resize.12.1------0.82------------
remove real,tuple0,unit,map,list,option,ref,zero,one,(>),(>=),abs,div,mod,const,is_nil,mem,is_none,hash,(!),next,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,numof_def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_nil_spec,is_none_spec,neq_spec,hash_nonneg,hash_eq,array'invariant,make_spec,bucket_spec,bucket_def,numof_eq,dummy_const
VC resize.12.1.0------------------0.02
VC resize.12.2------0.47------------
remove real,tuple0,unit,map,list,option,ref,zero,one,(>),(>=),abs,div,mod,const,is_nil,mem,is_none,hash,(!),next,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,numof_def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_nil_spec,is_none_spec,neq_spec,hash_nonneg,hash_eq,array'invariant,make_spec,bucket_spec,bucket_def,numof_eq,dummy_const
VC resize.12.2.0------------------0.02
VC resize.12.3---------------0.49---
VC resize.12.4------1.57------------
remove real,tuple0,unit,map,list,option,ref,zero,one,(>),abs,div,const,is_nil,mem,is_none,(!),next,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,numof_def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_nil_spec,is_none_spec,neq_spec,hash_nonneg,array'invariant,bucket_spec,numof_eq
VC resize.12.4.0------------------0.06
VC resize.12.5------0.12------------
remove real,tuple0,unit,map,list,option,ref,zero,one,(>),(>=),abs,div,mod,const,is_nil,mem,is_none,hash,(!),next,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,numof_def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_nil_spec,is_none_spec,neq_spec,hash_nonneg,hash_eq,array'invariant,make_spec,bucket_spec,bucket_def,numof_eq,dummy_const
VC resize.12.5.0---------0.03---------
VC resize.130.02------------------
VC resize.140.01------------------
VC resize.15---------------0.10---
VC resize.16------------0.04------
VC resize.17------------0.06------
VC resize.18---------------------
split_goal_right
VC resize.18.0------0.06------------
VC resize.190.01------------------
VC resize.200.01------------------
VC add---------------------
split_goal_right
VC add.00.01------------------
VC add.10.01------------------
VC add.20.01------------------
VC add.30.01------------------
VC add.40.01------------------
VC add.50.01------------------
VC add.6---------------0.18---
VC add.7------------0.06------
VC add.8------------------0.19
VC add.9---------------------
split_goal_right
VC add.9.0---------------------
unfold valid
VC add.9.0.0---------------------
split_goal_right
VC add.9.0.0.0------------0.08------
VC add.9.0.0.1---------------------
inline_all
VC add.9.0.0.1.0------------0.16------
VC add.9.0.0.2---------------------
introduce_premises
VC add.9.0.0.2.0---------------------
subst_all
VC add.9.0.0.2.0.0---------------------
case (i=i1)
VC add.9.0.0.2.0.0.0---0.03---------------
VC add.9.0.0.2.0.0.1---------------------
inline_all
VC add.9.0.0.2.0.0.1.0------------0.13------
VC add.9.0.0.3---------------------
split_all_full
VC add.9.0.0.3.0------------------0.96
VC add.9.0.0.4---------------------
split_all_full
VC add.9.0.0.4.0------------------0.91
VC add.9.0.0.5---------------------
inline_all
VC add.9.0.0.5.0------------------0.56
VC add.9.0.0.6---------------------
inline_all
VC add.9.0.0.6.0------------------0.19
VC add.9.0.0.7------------0.20------
VC add.100.01------------------
VC add.11------------0.05------
VC add.12------------0.06------
VC add.13------------0.11------
VC add.140.01------------------
VC copy---------2.03---------
VC find_dummy0.42------------------
VC delete---------------------
split_goal_right
VC delete.00.01------------------
VC delete.10.01------------------
VC delete.20.03------------------
VC delete.30.01------------------
VC delete.40.01------------------
VC delete.50.02------------------
VC delete.60.01------------------
VC delete.70.01------------------
VC delete.80.01------------------
VC delete.90.03------------------
VC delete.100.10------------------
VC delete.110.01------------------
VC delete.120.01------------------
VC delete.131.42------------------
VC delete.140.01------------------
VC delete.150.01------------------
VC delete.160.01------------------
VC delete.170.01------------------
VC delete.180.01------------------
VC delete.190.01------------------
VC delete.200.02------------------
VC delete.210.02------------------
VC delete.220.01------------------
VC delete.230.01------------------
VC delete.240.06------------------
VC delete.250.08------------------
VC delete.260.02------------------
VC delete.270.12------------------
VC delete.280.07------------------
VC delete.290.01------------------
VC delete.300.08------------------
VC delete.310.08------------------
VC delete.320.01------------------
VC delete.330.02------------------
VC delete.340.02------------------
VC delete.350.02------------------
VC delete.36---------------0.27---
VC delete.370.01------------------
VC delete.38---------------------
split_goal_right
VC delete.38.0------0.44------------
VC delete.38.1------0.90------------
VC delete.39------------0.15------
VC delete.400.01------------------
VC delete.410.02------------------
VC delete.420.01------------------
VC delete.43---------0.13---0.15---
VC remove---------------------
split_goal_right
VC remove.00.01------------------
VC remove.10.01------------------
VC remove.20.01------------------
VC remove.30.01------------------
VC remove.4---------------0.22---
VC remove.50.01------------------
VC remove.60.01------------------
VC remove.70.01------------------
VC remove.8---------------0.28---
VC remove.90.02------------------
VC remove.100.01------------------
VC remove.110.01------------------
VC remove.120.01------------------
VC remove.130.01------------------
VC remove.140.01------------------
VC remove.150.01------------------
VC remove.160.01------------------
VC remove.170.02------------------
VC remove.180.02------------------
VC remove.19------------0.15------
VC remove.203.41------------------
VC remove.21------------0.56------
VC remove.22------------------0.32
VC remove.23---------------0.02---
VC remove.240.01------------------
VC remove.25---------0.16---0.25---