types

HTable = map Location to CollisionBucket
inv x == forall a in set rng x &
         forall b,c in set a & hash(b) = hash(c);

Location = nat
inv x == x < 10;

CollisionBucket = set of Data;

Data = seq of char

functions

hash : Data -> Location
hash (d) == len d mod 10;

Init : () -> HTable
Init () == { i |-> {} | i in set {0,...,9} };

Insert : Data * HTable -> HTable
Insert (d, ht) == let hs = hash(d)
                  in ht ++ { hs |-> ht(hs) union {d} };

Find : Data * HTable -> bool
Find  (d, ht) == let hs = hash(d)
                 in hs in set dom ht and d in set ht(hs);

Remove : Data * HTable -> HTable
Remove (d, ht) == let hs = hash(d)
                  in ht ++ { hs |-> ht(hs) \ {d} }
pre hash(d) in set dom ht;

rep : set of Data -> HTable
rep (s) == if s = {} 
           then Init()
           else let e in set s
                in Insert(e, rep( s \ {e} ));

Abs : HTable -> set of Data
Abs (ht) == dunion { ht(i) | i in set dom ht }