## Hash table implementation

Minimal hash tables, without remove operation.

Authors: Jean-Christophe Filliâtre

Topics: Hash tables / Data Structures

Tools: Why3

```(* Hash table implementation.

These are minimal hash tables, without [remove] operation.

This is suitable to implement memo tables for instance.
One example of such a use is in max_matrix.mlw *)

(* The signature *)
module HashTable

use import option.Option
use import int.Int
use import map.Map

type t 'a 'b model { mutable contents: map 'a (option 'b) }

function ([]) (h: t 'a 'b) (k: 'a) : option 'b = Map.get h.contents k

val create (n:int) : t 'a 'b
requires { 0 < n } ensures { forall k: 'a. result[k] = None }

val clear (h: t 'a 'b) : unit writes {h}
ensures { forall k: 'a. h[k] = None }

val add (h: t 'a 'b) (k: 'a) (v: 'b) : unit writes {h}
ensures { h[k] = Some v /\ forall k': 'a. k' <> k -> h[k'] = (old h)[k'] }

exception Not_found

val find (h: t 'a 'b) (k: 'a) : 'b reads {h}
ensures { h[k] = Some result } raises { Not_found -> h[k] = None }

end

(* the implementation *)
module HashTableImpl

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

type t 'a 'b = { mutable contents: map 'a (option 'b);
data: array (list ('a, 'b)) }
invariant { length self.data > 0 }

function get (h: t 'a 'b) (k: 'a) : option 'b = Map.get h.contents k

function hash 'a : int

function idx (h: t 'a 'b) (k: 'a) : int =
mod (abs (hash k)) (length h.data)

lemma idx_bounds:
forall h: t 'a 'b, k: 'a.
0 < length h.data -> 0 <= idx h k < length h.data

(* [(k,v)] is the first pair in [l] with key [k] *)
predicate occurs_first (k: 'a) (v: 'b) (l: list ('a, 'b)) = match l with
| Nil            -> false
| Cons (k',v') r -> (k = k' /\ v = v') \/ (k <> k' /\ occurs_first k v r)
end

lemma mem_occurs_first:
forall k: 'a, v: 'b, l: list ('a, 'b).
occurs_first k v l -> mem (k, v) l

lemma cons_occurs_first:
forall k1: 'a, v1: 'b, l: list ('a, 'b). occurs_first k1 v1 l ->
forall k: 'a, v: 'b. k <> k1 -> occurs_first k1 v1 (Cons (k,v) l)

type t 'c 'b
(* h[k]=v iff (k,v) is the first pair for k in the bucket for k *)
invariant { forall k: 'c, v: 'b.
get self k = Some v <-> occurs_first k v self.data[idx self k] }
(* a pair (k,v) is always stored in the right bucket *)
invariant { forall k: 'c, v: 'b.
forall i: int. 0 <= i < length self.data ->
mem (k,v) self.data[i] -> i = idx self k }

let create (n:int)
requires { 0 < n }
ensures  { forall k: 'a. get result k = None }
= { contents = const None; data = make n (Nil: list ('a, 'b)) }

let clear (h: t 'a 'b)
ensures { forall k: 'a. get h k = None }
= fill h.data 0 (length h.data) Nil;
h.contents <- const None

let idx (h: t 'a 'b) (k: 'a)
ensures { result = idx h k }
= mod (abs (hash k)) (length h.data)

let add (h: t 'a 'b) (k: 'a) (v: 'b)
ensures { get h k = Some v }
ensures { forall k': 'a. k' <> k -> get h k' = get (old h) k' }
= let i = idx h k in
h.data[i] <- Cons (k,v) h.data[i];
h.contents <- Map.set h.contents k (Some v)

exception Not_found

let rec lookup (k: 'a) (l: list ('a, 'b)) : 'b
ensures { occurs_first k result l }
raises  { Not_found -> forall v: 'b. not (mem (k, v) l) }
= match l with
| Nil -> raise Not_found
| Cons (k', v) r -> if k = k' then v else lookup k r
end

let find (h: t 'a 'b) (k: 'a)
ensures { get h k = Some result }
raises  { Not_found -> get h k = None }
= let i = idx h k in
lookup k h.data[i]

end
```