hash tables as a separate example (in progress)

examples/programs/hash_tables.mlw

+
+(* 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) :
+    { 0 < n } t 'a 'b { forall k: 'a. result[k] = None }
+
+  val clear (h: t 'a 'b) :
+    {} unit writes h { forall k: 'a. h[k] = None }
+
+  val add (h: t 'a 'b) (k: 'a) (v: 'b) :
+    {}
+    unit writes h
+    { 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 raises Not_found
+    { h[k] = Some result } | 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 module array.Array
+
+  type t 'a 'b = {| mutable contents: map 'a (option 'b);
+                    data: array (list ('a, 'b)) |}
+
+  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)
+
+  (* [(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
+
+  predicate valid (h: t 'a 'b) =
+    length h.data > 0 /\
+    (forall k: 'a, v: 'b.
+       get h k = Some v <-> occurs_first k v h.data[idx h k]) /\
+    (forall k: 'a, v: 'b.
+     forall i: int. 0 <= i < length h.data ->
+       mem (k,v) h.data[i] -> i = idx h k)
+
+  lemma idx_bounds:
+    forall h: t 'a 'b. valid h -> forall k: 'a. 0 <= idx h k < length h.data
+
+  let create (n:int) =
+    { 0 < n }
+    {| contents = const None;
+       data = make n (Nil: list ('a, 'b)) |}
+    { valid result /\ forall k: 'a. get result k = None }
+
+  let clear (h: t 'a 'b) =
+    { valid h }
+    fill h.data 0 (length h.data) Nil;
+    h.contents <- const None
+    { valid h /\ forall k: 'a. get h k = None }
+
+  let add (h: t 'a 'b) (k: 'a) (v: 'b) =
+    { valid h }
+    let i = idx h k in
+    h.data[i] <- Cons (k,v) h.data[i];
+    h.contents <- Map.set h.contents k (Some v)
+    { valid h &&
+      get h k = Some v /\ forall k': 'a. k' <> k -> get h k' = get (old h) k' }
+
+  exception Not_found
+
+  let rec lookup (k: 'a) (l: list ('a, 'b)) : 'b =
+    {}
+    match l with
+    | Nil -> raise Not_found
+    | Cons (k', v) r -> if k = k' then v else lookup k r
+    end
+    { occurs_first k result l }
+    | Not_found -> { forall v: 'b. not (mem (k, v) l) }
+
+  let find (h: t 'a 'b) (k: 'a) =
+    { valid h }
+    let i = idx h k in
+    lookup k h.data[i]
+    { get h k = Some result } | Not_found -> { get h k = None }
+
+end
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../.. examples/programs/hash_tables.gui"
+End:
+*)

examples/programs/hash_tables/hash_tables_WP_HashTableImpl_WP_parameter_find_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import ZOdiv.
+Definition unit  := unit.
+
+Parameter qtmark : Type.
+
+Parameter at1: forall (a:Type), a -> qtmark -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a -> a.
+
+Implicit Arguments old.
+
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+Inductive option (a:Type) :=
+  | None : option a
+  | Some : a -> option a.
+Set Contextual Implicit.
+Implicit Arguments None.
+Unset Contextual Implicit.
+Implicit Arguments Some.
+
+Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
+  (x <= y)%Z).
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter const: forall (b:Type) (a:Type), b -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (const b1:(map a b)) a1) = b1).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Inductive array (a:Type) :=
+  | mk_array : Z -> (map Z a) -> array a.
+Implicit Arguments mk_array.
+
+Definition elts (a:Type)(u:(array a)): (map Z a) :=
+  match u with
+  | (mk_array _ elts1) => elts1
+  end.
+Implicit Arguments elts.
+
+Definition length (a:Type)(u:(array a)): Z :=
+  match u with
+  | (mk_array length1 _) => length1
+  end.
+Implicit Arguments length.
+
+Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
+Implicit Arguments get1.
+
+Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
+  match a1 with
+  | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
+  end.
+Implicit Arguments set1.
+
+Inductive t (a:Type)
+  (b:Type) :=
+  | mk_t : (map a (option b)) -> (array (list (a* b)%type)) -> t a b.
+Implicit Arguments mk_t.
+
+Definition contents (a:Type) (b:Type)(u:(t a b)): (map a (option b)) :=
+  match u with
+  | (mk_t contents1 _) => contents1
+  end.
+Implicit Arguments contents.
+
+Definition data (a:Type) (b:Type)(u:(t a b)): (array (list (a* b)%type)) :=
+  match u with
+  | (mk_t _ data1) => data1
+  end.
+Implicit Arguments data.
+
+Definition get2 (a:Type) (b:Type)(h:(t a b)) (k:a): (option b) :=
+  (get (contents h) k).
+Implicit Arguments get2.
+
+Parameter hash: forall (a:Type), a -> Z.
+
+Implicit Arguments hash.
+
+Definition idx (a:Type) (b:Type)(h:(t a b)) (k:a): Z :=
+  (ZOmod (Zabs (hash k)) (length (data h))).
+Implicit Arguments idx.
+
+Set Implicit Arguments.
+Fixpoint occurs_first (a:Type) (b:Type)(k:a) (v:b) (l:(list (a*
+  b)%type)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons (kqt, vqt) r) => ((k = kqt) /\ (v = vqt)) \/ ((~ (k = kqt)) /\
+      (occurs_first k v r))
+  end.
+Unset Implicit Arguments.
+
+Axiom mem_occurs_first : forall (a:Type) (b:Type), forall (k:a) (v:b)
+  (l:(list (a* b)%type)), (occurs_first k v l) -> (mem (k, v) l).
+
+Definition valid (a:Type) (b:Type)(h:(t a b)): Prop :=
+  (0%Z <  (length (data h)))%Z /\ ((forall (k:a) (v:b), ((get2 h
+  k) = (Some v)) <-> (occurs_first k v (get1 (data h) (idx h k)))) /\
+  forall (k:a) (v:b), forall (i:Z), ((0%Z <= i)%Z /\
+  (i <  (length (data h)))%Z) -> ((mem (k, v) (get1 (data h) i)) ->
+  (i = (idx h k)))).
+Implicit Arguments valid.
+
+Axiom idx_bounds : forall (a:Type) (b:Type), forall (h:(t a b)), (valid h) ->
+  forall (k:a), (0%Z <= (idx h k))%Z /\ ((idx h k) <  (length (data h)))%Z.
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem WP_parameter_find : forall (a:Type) (b:Type), forall (h:Z),
+  forall (k:a), forall (rho:(map Z (list (a* b)%type))), forall (rho1:(map a
+  (option b))), (valid (mk_t rho1 (mk_array h rho))) ->
+  (((0%Z <= (ZOmod (Zabs (hash k)) h))%Z /\
+  ((ZOmod (Zabs (hash k)) h) <  h)%Z) -> let result := (get rho
+  (ZOmod (Zabs (hash k)) h)) in ((forall (result1:b), (occurs_first k result1
+  result) -> ((get rho1 k) = (Some result1))) -> ((forall (v:b), ~ (mem (k,
+  v) result)) -> ((get rho1 k) = (None :(option b)))))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros a b h k rho.
+unfold valid.
+pose (i := (Zabs (hash k) mod h)).
+unfold get1; simpl.
+intuition.
+generalize (H0 k); clear H0.
+generalize (H6 k); clear H6.
+unfold get2; simpl; intuition.
+destruct (get rho1 k); auto.
+elim (H2 b0); clear H2.
+generalize (H4 b0); clear H4.
+intuition.
+apply mem_occurs_first; auto.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/hash_tables/hash_tables_WP_HashTableImpl_mem_occurs_first_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import ZOdiv.
+Definition unit  := unit.
+
+Parameter qtmark : Type.
+
+Parameter at1: forall (a:Type), a -> qtmark -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a -> a.
+
+Implicit Arguments old.
+
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+Inductive option (a:Type) :=
+  | None : option a
+  | Some : a -> option a.
+Set Contextual Implicit.
+Implicit Arguments None.
+Unset Contextual Implicit.
+Implicit Arguments Some.
+
+Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
+  (x <= y)%Z).
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter const: forall (b:Type) (a:Type), b -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (const b1:(map a b)) a1) = b1).
+
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+Set Implicit Arguments.
+Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons y r) => (x = y) \/ (mem x r)
+  end.
+Unset Implicit Arguments.
+
+Inductive array (a:Type) :=
+  | mk_array : Z -> (map Z a) -> array a.
+Implicit Arguments mk_array.
+
+Definition elts (a:Type)(u:(array a)): (map Z a) :=
+  match u with
+  | (mk_array _ elts1) => elts1
+  end.
+Implicit Arguments elts.
+
+Definition length (a:Type)(u:(array a)): Z :=
+  match u with
+  | (mk_array length1 _) => length1
+  end.
+Implicit Arguments length.
+
+Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
+Implicit Arguments get1.
+
+Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
+  match a1 with
+  | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
+  end.
+Implicit Arguments set1.
+
+Inductive t (a:Type)
+  (b:Type) :=
+  | mk_t : (map a (option b)) -> (array (list (a* b)%type)) -> t a b.
+Implicit Arguments mk_t.
+
+Definition contents (a:Type) (b:Type)(u:(t a b)): (map a (option b)) :=
+  match u with
+  | (mk_t contents1 _) => contents1
+  end.
+Implicit Arguments contents.
+
+Definition data (a:Type) (b:Type)(u:(t a b)): (array (list (a* b)%type)) :=
+  match u with
+  | (mk_t _ data1) => data1
+  end.
+Implicit Arguments data.
+
+Definition get2 (a:Type) (b:Type)(h:(t a b)) (k:a): (option b) :=
+  (get (contents h) k).
+Implicit Arguments get2.
+
+Parameter hash: forall (a:Type), a -> Z.
+
+Implicit Arguments hash.
+
+Definition idx (a:Type) (b:Type)(h:(t a b)) (k:a): Z :=
+  (ZOmod (Zabs (hash k)) (length (data h))).
+Implicit Arguments idx.
+
+Set Implicit Arguments.
+Fixpoint occurs_first (a:Type) (b:Type)(k:a) (v:b) (l:(list (a*
+  b)%type)) {struct l}: Prop :=
+  match l with
+  | Nil => False
+  | (Cons (kqt, vqt) r) => ((k = kqt) /\ (v = vqt)) \/ ((~ (k = kqt)) /\
+      (occurs_first k v r))
+  end.
+Unset Implicit Arguments.
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem mem_occurs_first : forall (a:Type) (b:Type), forall (k:a) (v:b)
+  (l:(list (a* b)%type)), (occurs_first k v l) -> (mem (k, v) l).
+(* YOU MAY EDIT THE PROOF BELOW *)
+induction l; simpl; intuition.
+destruct a0; intuition.
+subst; left; auto.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/max_matrix.mlw

@@ -14,7 +14,7 @@
 
    The following code implements such a solution. Sets of integers are
    provided in theory Bitset. Hash tables for memoization are provided
-   in module HashTable (signature) and HashTableImpl (implementation).
+   in module HashTable (see file hash_tables.mlw for an implementation).
    Code for f is in module MaxMatrixMemo (mutually recursive functions
    maximum and memo).
 *)
@@ -92,79 +92,6 @@ module HashTable
 
 end
 
-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 module array.Array
-
-  type t 'a 'b = array (list ('a, 'b))
-
-  function get (h: t 'a 'b) (k: 'a) : option 'b
-
-  axiom get_None:
-    forall h: t 'a 'b, k: 'a.
-    get h k = None <->
-    (forall i: int. 0 <= i < length h -> forall v: 'b. not (mem (k, v) h[i]))
-
-  axiom get_Some:
-    forall h: t 'a 'b, k: 'a, v: 'b.
-    get h k = Some v <->
-    exists i: int. 0 <= i < length h /\ mem (k,v) h[i]
-
-  function hash 'a : int
-
-  function idx (h: t 'a 'b) (k: 'a) : int =
-    mod (abs (hash k)) (length h)
-
-  predicate inv (h: t 'a 'b) =
-    length h > 0 /\
-    forall i: int. 0 <= i < length h ->
-    forall k: 'a, v: 'b. mem (k,v) h[i] -> idx h k = i
-
-  lemma idx_bounds:
-    forall h: t 'a 'b. inv h -> forall k: 'a. 0 <= idx h k < length h
-
-  let create (n:int) =
-    { 0 < n }
-    make n (Nil: list ('a, 'b))
-    { inv result /\ forall k: 'a. get result k = None }
-
-  let clear (h: t 'a 'b) =
-    { inv h }
-    fill h 0 (length h) Nil
-    { inv h /\ forall k: 'a. get h k = None }
-
-  let add (h: t 'a 'b) (k: 'a) (v: 'b) =
-    { inv h }
-    let i = idx h k in
-    h[i] <- Cons (k,v) h[i]
-    { inv h &&
-      get h k = Some v /\ forall k': 'a. k' <> k -> get h k' = get (old h) k' }
-
-  exception Not_found
-
-  let rec lookup (k: 'a) (l: list ('a, 'b)) : 'b =
-    {}
-    match l with
-    | Nil -> raise Not_found
-    | Cons (k', v) r -> if k = k' then v else lookup k r
-    end
-    { mem (k, result) l } | Not_found -> { forall v: 'b. not (mem (k, v) l) }
-
-  let find (h: t 'a 'b) (k: 'a) =
-    { inv h }
-    let i = idx h k in
-    lookup k h[i]
-    { get h k = Some result } | Not_found -> { get h k = None }
-
-end
-
 module MaxMatrixMemo
 
   use import int.Int

modules/hashtbl.mlw

 
+(* Hash tables à la OCaml: each key is mapped to a *stack* of values,
+   with [add h k v] pushing a new value [v] for key [k],
+   and [remove h k] popping a value for key [key]. *)
+
 module Hashtbl
 
   use import list.List
@@ -51,9 +55,9 @@ module Hashtbl
     { forall k: key. result[k] = h[k] }
 
   val remove (h: t 'a) (k: key) :
-    { h[k] <> Nil }
+    {}
     unit writes h
-    { (match (old h)[k] with Nil -> false | Cons _ l -> h[k] =l end) /\
+    { h[k] = match (old h)[k] with Nil -> Nil | Cons _ l -> l end /\
       forall k': key. k' <> k -> h[k'] = (old h)[k'] }
 
   val replace (h: t 'a) (k: key) (v: 'a) :