## Hash table implementation

Topics: Data Structures

Tools: Why3

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

```(* Hash table implementation

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

module HashtblImpl

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

type key

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

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

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

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

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

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

let clear (h: t 'a) : unit
writes  { h.size, h.data.elts, h.view }
ensures { h.view = Const.const None }
=
h.size <- 0;
fill h.data 0 (length h.data) Nil;
h.view <- Const.const None

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 }
variant  { l }
= 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

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 }
= match l with
| Nil -> None
| Cons (k', v) r -> if eq k k' then Some v else list_find k r
end

let find (h: t 'a) (k: key) : option 'a
ensures { result = Map.get h.view k }
=
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.
mem (k',v) result <-> mem (k',v) l /\ k' <> k }
= match l with
| Nil -> Nil
| Cons ((k', _) as p) r ->
if eq k k' then list_remove k r else Cons p (list_remove k r)
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 ->
Map.get h.view k' = Map.get (old h.view) k' }
= let i = bucket k (length h.data) in
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
writes  { h, h.data.elts }
ensures { Map.get h.view k = Some v }
ensures { forall k': key. k' <> k ->
Map.get h.view k' = Map.get (old h.view) k' }
=
if h.size = length h.data then resize h;
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)

(*
let alias (h: t int) (k: key) : unit =
let old_data = h.data in