Commit 596e2a84 authored by Andrei Paskevich's avatar Andrei Paskevich

new hash table implementation in examples

parent 89bf7951
(* 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
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import ZOdiv.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive option (a:Type) :=
| None : option a
| Some : a -> option a.
Set Contextual Implicit.
Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.
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 (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
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.
(* Why3 assumption *)
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.
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
(* Why3 assumption *)
Definition elts (a:Type)(v:(array a)): (map Z a) :=
match v with
| (mk_array x x1) => x1
end.
Implicit Arguments elts.
(* Why3 assumption *)
Definition length (a:Type)(v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
Implicit Arguments length.
(* Why3 assumption *)
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
(* Why3 assumption *)
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
(mk_array (length a1) (set (elts a1) i v)).
Implicit Arguments set1.
(* Why3 assumption *)
Inductive t (a:Type)
(b:Type) :=
| mk_t : (map a (option b)) -> (array (list (a* b)%type)) -> t a b.
Implicit Arguments mk_t.
(* Why3 assumption *)
Definition data (a:Type) (b:Type)(v:(t a b)): (array (list (a* b)%type)) :=
match v with
| (mk_t x x1) => x1
end.
Implicit Arguments data.
(* Why3 assumption *)
Definition contents (a:Type) (b:Type)(v:(t a b)): (map a (option b)) :=
match v with
| (mk_t x x1) => x
end.
Implicit Arguments contents.
(* Why3 assumption *)
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.
(* Why3 assumption *)
Definition idx (a:Type) (b:Type)(h:(t a b)) (k:a): Z :=
(ZOmod (Zabs (hash k)) (length (data h))).
Implicit Arguments idx.
(* Why3 assumption *)
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 (k', v') r) => ((k = k') /\ (v = v')) \/ ((~ (k = k')) /\
(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).
Axiom cons_occurs_first : forall (a:Type) (b:Type), forall (k1:a) (v1:b)
(l:(list (a* b)%type)), (occurs_first k1 v1 l) -> forall (k:a) (v:b),
(~ (k = k1)) -> (occurs_first k1 v1 (Cons (k, v) l)).
(* Why3 assumption *)
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.
Require Import Classical.
(* Why3 goal *)
Theorem WP_parameter_add : forall (a:Type) (b:Type), forall (h:Z) (k:a)
(v:b), forall (rho:(map Z (list (a* b)%type))) (rho1:(map a (option b))),
((0%Z < (length (data (mk_t rho1 (mk_array h rho)))))%Z /\ ((forall (k1:a)
(v1:b), ((get2 (mk_t rho1 (mk_array h rho)) k1) = (Some v1)) <->
(occurs_first k1 v1 (get1 (data (mk_t rho1 (mk_array h rho)))
(idx (mk_t rho1 (mk_array h rho)) k1)))) /\ forall (k1:a) (v1:b),
forall (i:Z), ((0%Z <= i)%Z /\ (i < (length (data (mk_t rho1 (mk_array h
rho)))))%Z) -> ((mem (k1, v1) (get1 (data (mk_t rho1 (mk_array h rho)))
i)) -> (i = (idx (mk_t rho1 (mk_array h rho)) k1))))) -> let i :=
(ZOmod (Zabs (hash k)) h) in ((((0%Z < i)%Z \/ (0%Z = i)) /\ (i < h)%Z) ->
((((0%Z < i)%Z \/ (0%Z = i)) /\ (i < h)%Z) -> forall (o:(map Z (list (a*
b)%type))), (o = (set rho i (Cons (k, v) (get rho i)))) ->
forall (rho2:(map a (option b))), (rho2 = (set rho1 k (Some v))) ->
forall (k1:a) (v1:b), ((get2 (mk_t rho2 (mk_array h o)) k1) = (Some v1)) ->
(occurs_first k1 v1 (get1 (data (mk_t rho2 (mk_array h o))) (idx (mk_t rho2
(mk_array h o)) k1))))).
unfold get1; simpl; intros.
assert (case: (k1=k \/ k1<>k)) by apply classic; destruct case.
(* k1 = k *)
subst k1.
subst rho2.
unfold get2 in H4; simpl in H4.
rewrite Select_eq in H4; auto.
injection H4; intro; subst v1; clear H4.
unfold idx; simpl.
subst o; rewrite Select_eq.
red; intuition.
auto.
(* k1 <> k *)
subst rho2.
unfold idx; simpl.
unfold get2 in H4; simpl in H4.
rewrite Select_neq in H4; auto.
subst o.
set (i := (Zabs (hash k) mod h)).
set (i1 := (Zabs (hash k1) mod h)).
assert (case: (i1=i \/ i1<>i)) by omega; destruct case.
(* i1 = i *)
subst i1.
rewrite Select_eq; auto.
simpl.
right; split; auto.
destruct H.
destruct H3.
rewrite <- H2.
destruct (H3 k1 v1); clear H3.
unfold idx in H7; simpl in H7.
subst i.
apply H7.
unfold get2; simpl.
auto.
(* i1 <> i *)
rewrite Select_neq; auto.
destruct H.
destruct H3.
destruct (H3 k1 v1); clear H3.
unfold idx in H7; simpl in H7.
subst i1.
apply H7.
unfold get2; simpl.
auto.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import ZOdiv.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive option (a:Type) :=
| None : option a
| Some : a -> option a.
Implicit Arguments None [[a]].
Implicit Arguments Some [[a]].
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall {a:Type} {b:Type}, (map a b) -> a -> b.
Parameter set: forall {a:Type} {b:Type}, (map a b) -> a -> b -> (map a b).
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 {a:Type} {b:Type}, b -> (map a b).
Axiom Const : forall {a:Type} {b:Type}, forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
(* Why3 assumption *)
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.
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type}(v:(array a)): (map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type}(v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get1 {a:Type}(a1:(array a)) (i:Z): a := (get (elts a1) i).
(* Why3 assumption *)
Definition set1 {a:Type}(a1:(array a)) (i:Z) (v:a): (array a) :=
(mk_array (length a1) (set (elts a1) i v)).
(* Why3 assumption *)
Inductive t (a:Type)
(b:Type) :=
| mk_t : (map a (option b)) -> (array (list (a* b)%type)) -> t a b.
Implicit Arguments mk_t [[a]
[b]].
(* Why3 assumption *)
Definition data {a:Type} {b:Type}(v:(t a b)): (array (list (a* b)%type)) :=
match v with
| (mk_t x x1) => x1
end.
(* Why3 assumption *)
Definition contents {a:Type} {b:Type}(v:(t a b)): (map a (option b)) :=
match v with
| (mk_t x x1) => x
end.
(* Why3 assumption *)
Definition get2 {a:Type} {b:Type}(h:(t a b)) (k:a): (option b) :=
(get (contents h) k).
Parameter hash: forall {a:Type}, a -> Z.
(* Why3 assumption *)
Definition idx {a:Type} {b:Type}(h:(t a b)) (k:a): Z :=
(ZOmod (Zabs (hash k)) (length (data h))).
(* Why3 assumption *)
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 (k', v') r) => ((k = k') /\ (v = v')) \/ ((~ (k = k')) /\
(occurs_first k v r))
end.
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).
Axiom cons_occurs_first : forall {a:Type} {b:Type}, forall (k1:a) (v1:b)
(l:(list (a* b)%type)), (occurs_first k1 v1 l) -> forall (k:a) (v:b),
(~ (k = k1)) -> (occurs_first k1 v1 (Cons (k, v) l)).
(* Why3 assumption *)
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)))).
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.
Require Import Classical.
(* Why3 goal *)
Theorem WP_parameter_add : forall {a:Type} {b:Type}, forall (h:Z) (k:a)
(v:b), forall (rho:(map Z (list (a* b)%type))) (rho1:(map a (option b))),
((0%Z < (length (data (mk_t rho1 (mk_array h rho)))))%Z /\ ((forall (k1:a)
(v1:b), ((get2 (mk_t rho1 (mk_array h rho)) k1) = (Some v1)) <->
(occurs_first k1 v1 (get1 (data (mk_t rho1 (mk_array h rho)))
(idx (mk_t rho1 (mk_array h rho)) k1)))) /\ forall (k1:a) (v1:b),
forall (i:Z), ((0%Z <= i)%Z /\ (i < (length (data (mk_t rho1 (mk_array h
rho)))))%Z) -> ((mem (k1, v1) (get1 (data (mk_t rho1 (mk_array h rho)))
i)) -> (i = (idx (mk_t rho1 (mk_array h rho)) k1))))) -> let i :=
(ZOmod (Zabs (hash k)) h) in ((((0%Z < i)%Z \/ (0%Z = i)) /\ (i < h)%Z) ->
((((0%Z < i)%Z \/ (0%Z = i)) /\ (i < h)%Z) -> forall (o:(map Z (list (a*
b)%type))), (o = (set rho i (Cons (k, v) (get rho i)))) ->
forall (rho2:(map a (option b))), (rho2 = (set rho1 k (Some v))) ->
forall (k1:a) (v1:b), forall (i1:Z), ((0%Z <= i1)%Z /\
(i1 < (length (data (mk_t rho2 (mk_array h o)))))%Z) -> ((mem (k1, v1)
(get1 (data (mk_t rho2 (mk_array h o))) i1)) -> (i1 = (idx (mk_t rho2
(mk_array h o)) k1))))).
intros.
set (ik := (Zabs (hash k) mod h)).
simpl in H4.
assert (case: (i1 = ik \/ i1<>ik)) by omega; destruct case.
(* i = ik *)
subst rho2.
simpl in H5.
subst o.
unfold get1 in H5; simpl in H5.
rewrite Select_eq in H5; auto.
unfold idx; simpl.
assert (case: (k1,v1)=(k,v) \/ (k1,v1)<>(k,v)) by apply classic; destruct case.
(* k1,v1 = k,v *)
injection H2; intros; subst. auto.
(* k1,v1 <> k,v *)
inversion H5.
absurd ((k1,v1)=(k,v)); auto.
fold @mem in H3.
destruct H.
destruct H7.
clear H7.
simpl in H8.
subst ik.
apply (H8 k1 v1 i1); auto.
subst i1; unfold get1; simpl.
assumption.
(* i <> ik *)
subst o.
unfold idx; simpl.
unfold get1 in H5; simpl in H5.
rewrite Select_neq in H5; auto.
destruct H.
destruct H2.
clear H2.
simpl in H7.
apply (H7 k1 v1 i1); auto.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive option (a:Type) {a_WT:WhyType a} :=
| None : option a
| Some : a -> option a.
Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
Existing Instance option_WhyType.
Implicit Arguments None [[a] [a_WT]].
Implicit Arguments Some [[a] [a_WT]].
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
(* Why3 assumption *)
Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v:(map.Map.map Z a))).
(* Why3 assumption *)
Inductive t (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b} :=
| mk_t : (map.Map.map a (option b)) -> (array (list (a* b)%type)) -> t a b.
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b},
WhyType (t a b).
Existing Instance t_WhyType.