why3/examples/hashtbl_impl.mlw

(* 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 }
    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
    add h k 42;
    old_data[0] <- Nil
*)
end