examples/hashtbl_impl.mlw

   1
   2 (* Hash table implementation
   3
   4    Jean-Christophe Filliâtre (CNRS)
   5    Andrei Paskevich (Univ Paris Sud) *)
   6
   7 module HashtblImpl
   8
   9   use int.Int
  10   use int.ComputerDivision
  11   use option.Option
  12   use list.List
  13   use list.Mem
  14   use map.Map
  15   use map.Const
  16   use array.Array
  17
  18   type key
  19
  20   val eq (x y : key) : bool
  21     ensures { result <-> x = y }
  22
  23   val function hash key : int
  24     ensures { 0 <= result }
  25
  26   let function bucket (k: key) (n: int) : int
  27     requires { 0 < n }
  28     ensures { 0 <= result < n }
  29   = mod (hash k) n
  30
  31   lemma bucket_bounds:
  32     forall n: int. 0 < n ->
  33     forall k: key. 0 <= bucket k n < n
  34
  35   predicate in_data (k: key) (v: 'a) (d: array (list (key, 'a))) =
  36     mem (k,v) d[bucket k (length d)]
  37
  38   predicate good_data (k: key) (v: 'a)
  39       (m: map key (option 'a)) (d: array (list (key, 'a))) =
  40     Map.get m k = Some v <-> in_data k v d
  41
  42   predicate good_hash (d: array (list (key, 'a))) (i: int) =
  43     forall k: key, v: 'a. mem (k,v) d[i] -> bucket k (length d) = i
  44
  45   type t 'a = { mutable size: int;   (* total number of elements *)
  46                 mutable data: array (list (key, 'a)); (* buckets *)
  47           ghost mutable view: map key (option 'a); (* pure model *) }
  48
  49     invariant { 0 < length data }
  50     invariant {
  51       forall i: int. 0 <= i < length data -> good_hash data i }
  52     invariant { forall k: key, v: 'a. good_data k v view data }
  53     by { size = 0; data = make 1 Nil; view = Const.const None }
  54
  55   let create (n: int) : t 'a
  56     requires { 1 <= n }
  57     ensures  { result.view = Const.const None }
  58   =
  59     { size = 0; data = make n Nil; view = Const.const None }
  60
  61   let clear (h: t 'a) : unit
  62     writes  { h.size, h.data.elts, h.view }
  63     ensures { h.view = Const.const None }
  64   =
  65     h.size <- 0;
  66     fill h.data 0 (length h.data) Nil;
  67     h.view <- Const.const None
  68
  69   let resize (h: t 'a) : unit
  70     writes  { h.data }
  71   =
  72     let odata = h.data in
  73     let osize = length odata in
  74     let nsize = 2 * osize + 1 in
  75     let ndata = make nsize Nil in
  76     let rec rehash (ghost i : int) l
  77       requires { forall k: key, v: 'a. mem (k,v) l -> bucket k osize = i }
  78       requires { forall j: int. 0 <= j < nsize -> good_hash ndata j }
  79       requires { forall k: key, v: 'a.
  80         if 0 <= bucket k osize < i then good_data k v h.view ndata
  81         else if bucket k osize = i then
  82           (Map.get h.view k = Some v <-> mem (k,v) l \/ in_data k v ndata)
  83         else not in_data k v ndata }
  84       ensures  { forall j: int. 0 <= j < nsize -> good_hash ndata j }
  85       ensures  { forall k: key, v: 'a.
  86         if 0 <= bucket k osize <= i then good_data k v h.view ndata
  87         else not in_data k v ndata }
  88       variant  { l }
  89     = match l with
  90       | Nil -> ()
  91       | Cons (k, v) r ->
  92           let b = bucket k nsize in
  93           ndata[b] <- Cons (k, v) (ndata[b]);
  94           rehash i r
  95     end in
  96     for i = 0 to osize - 1 do
  97       invariant { forall j: int. 0 <= j < nsize -> good_hash ndata j }
  98       invariant { forall k: key, v: 'a.
  99         if 0 <= bucket k osize < i then good_data k v h.view ndata
 100         else not in_data k v ndata }
 101       rehash i odata[i]
 102     done;
 103     h.data <- ndata
 104
 105   let rec list_find (k: key) (l: list (key, 'a)) : option 'a
 106     variant { l }
 107     ensures { match result with
 108               | None -> forall v: 'a. not (mem (k, v) l)
 109               | Some v -> mem (k, v) l
 110               end }
 111   = match l with
 112     | Nil -> None
 113     | Cons (k', v) r -> if eq k k' then Some v else list_find k r
 114     end
 115
 116   let find (h: t 'a) (k: key) : option 'a
 117     ensures { result = Map.get h.view k }
 118   =
 119     let i = bucket k (length h.data) in
 120     list_find k h.data[i]
 121
 122   let rec list_remove (k: key) (l: list (key, 'a)) : list (key, 'a)
 123     variant { l }
 124     ensures { forall k': key, v: 'a.
 125                 mem (k',v) result <-> mem (k',v) l /\ k' <> k }
 126   = match l with
 127     | Nil -> Nil
 128     | Cons ((k', _) as p) r ->
 129         if eq k k' then list_remove k r else Cons p (list_remove k r)
 130     end
 131
 132   let remove (h: t 'a) (k: key) : unit
 133     writes  { h.data.elts, h.view, h.size }
 134     ensures { Map.get h.view k = None }
 135     ensures { forall k': key. k' <> k ->
 136                 Map.get h.view k' = Map.get (old h.view) k' }
 137   = let i = bucket k (length h.data) in
 138     let l = h.data[i] in
 139     match list_find k l with
 140     | None ->
 141         ()
 142     | Some _ ->
 143         h.data[i] <- list_remove k l;
 144         h.size <- h.size - 1;
 145         h.view <- Map.set h.view k None
 146     end
 147
 148   let add (h: t 'a) (k: key) (v: 'a) : unit
 149     writes  { h }
 150     ensures { Map.get h.view k = Some v }
 151     ensures { forall k': key. k' <> k ->
 152                 Map.get h.view k' = Map.get (old h.view) k' }
 153   =
 154     if h.size = length h.data then resize h;
 155     remove h k;
 156     let i = bucket k (length h.data) in
 157     h.data[i] <- Cons (k, v) h.data[i];
 158     h.size <- h.size + 1;
 159     h.view <- Map.set h.view k (Some v)
 160
 161 (*
 162   let alias (h: t int) (k: key) : unit =
 163     let old_data = h.data in
 164     add h k 42;
 165     old_data[0] <- Nil
 166 *)
 167 end