## Hash tables with linear probing

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
```