Library RefAlgebraImplem_class
Require Export AlgebraType.
Definition PfCl := FiniteSet WordSize.
Inductive RelCl (h1 h2 : Heap) : Prop :=
RelCl_def :
(forall loc, h1 loc <> None -> h2 loc <> None) ->
(forall loc o1 o2, h1 loc = Some o1 ->
h2 loc = Some o2 -> class o1 = class o2) ->
RelCl h1 h2.
Lemma RelCl_refl : forall h, RelCl h h.
Proof.
constructor; auto; intros.
rewrite H in H0; injection H0; intros.
subst; auto.
Qed.
Hint Resolve RelCl_refl.
Lemma RelCl_same_class : forall h loc o',
(forall o, h loc = Some o -> class o = class o') ->
RelCl h (substHeap h loc o').
Proof.
intros; constructor; unfold substHeap.
intros loc' H1; case Location_dec; intros; discriminate || auto.
intros loc' o1 o2; case Location_dec; intros.
injection H1; clear H1; intros; subst; auto.
rewrite H0 in H1; injection H1; intros; subst; auto.
Qed.
Definition gammaCl (h:Heap) (s:PfCl) (loc:Location) : Prop :=
s = None \/
(h loc <> None /\
forall o, h loc = Some o -> in_set (class o) s = true).
Definition gammaRefCl : Heap -> Gamma (PowPoset Location) (LatticeFiniteSet WordSize).
intros h.
refine (gamma_constr (PowPoset Location) (LatticeFiniteSet WordSize)
(gammaCl h)
_).
intros b1 b2 H loc.
inversion_clear H; intros.
left; auto.
destruct H.
discriminate H.
destruct H; right; split; auto.
intros.
apply in_set_monotone with (Some f1); try constructor; auto.
Defined.
Definition gammaTopRefCl : Heap -> GammaTop (PowPoset Location) (LatticeFiniteSet WordSize).
intros h.
refine (gammatop_constr (gammaRefCl h) _).
intros; simpl.
intros; left; auto.
Defined.
Definition gammaTopBestRefCl : Heap -> GammaBestTop Location LatticeAtomFiniteSet.
intros h.
refine (gammabesttop_constr LatticeAtomFiniteSet (gammaTopRefCl h) _ _ ).
simpl; intros.
destruct b as [S|]; auto; intros.
destruct H.
discriminate H.
destruct H.
destruct H0.
discriminate H0.
destruct H0.
CaseEq (h a); intros.
apply in_set_eq with (class c); auto.
apply in_set_singleton; auto.
elim H; auto.
simpl; intros.
destruct H.
elim H0; auto.
destruct H.
CaseEq (h a); intros.
exists (class c).
simpl; right; split; auto.
intros.
rewrite H3 in H2; injection H2; intros; subst.
apply in_singleton.
elim H; auto.
Defined.
Definition RefAlgebraCl (P:Program) : Ref.Connect P.
refine (fun P => Ref.Build_Connect
RelCl
(fun tr => (hSt (currentState tr)))
gammaTopBestRefCl _
(fun cl pc => (singleton cl)) _ _ _ _).
intros h1 h2 H s loc H1.
inversion_clear H; destruct H1.
left; auto.
destruct H; right; split; auto.
intros.
CaseEq (h1 loc); intros.
rewrite <- (H2 _ _ _ H4 H3); auto.
elim H; auto.
intros tr1 tr2 cl pc Hsem H loc H1.
inversion_clear H1.
inversion_clear H0.
inversion_clear Hsem; simpl.
CaseEq (currentState tr1); intros.
rewrite H4 in H; rewrite H4 in H2; rewrite H4 in H0; simpl in *; subst.
inversion_clear H0.
right; split; subst.
simpl; unfold substHeap; case Location_dec; intros; auto.
discriminate.
simpl hSt.
intros o'; unfold substHeap; case Location_dec; intros; auto.
injection H0; clear H0; intros; subst.
unfold def; simpl class.
generalize (searchClass_rec_in_l_classname _ _ _ H2); intros.
apply in_singleton_eq; auto.
intros tr1 tr2 r H; inversion_clear H.
CaseEq (currentState tr1); intros h1 pc1 l1 s1 Heq; rewrite Heq in H0.
inversion_clear H0; simpl; auto.
subst; apply RelCl_same_class.
intros.
generalize (searchClass_rec_in_l_classname _ _ _ H1); intros.
generalize (searchClass_in_class _ _ _ H1); intros.
rewrite (newObject_specif _ _ _ h1 H3 H2) in H0.
discriminate H0.
apply RelCl_same_class.
intros.
rewrite H0 in H1; injection H1; intros; subst.
rewrite class_substField; auto.
intros tr1 tr2 r H Hr; inversion_clear H.
CaseEq (currentState tr1); intros h1 pc1 l1 s1 Heq; rewrite Heq in H0.
inversion_clear H0 in Hr; simpl; auto.
inversion_clear Hr.
constructor.
intros loc0; unfold substHeap; case Location_dec; intros.
subst; rewrite H1; discriminate.
auto.
intros loc0; unfold substHeap; case Location_dec; intros.
subst; rewrite H3 in H1; injection H1; intros; subst.
injection H0; intros; subst.
rewrite class_substField; auto.
rewrite H0 in H3; injection H3; intros; subst; auto.
intros.
inversion_clear H in H0 H1 H2.
CaseEq (currentState tr1); intros h1' pc1 l1 s1 Heq.
rewrite Heq in H0; rewrite Heq in H3; simpl in *; subst.
clear Heq; inversion_clear H3 in H1 H2; simpl in *.
destruct H2.
left; auto.
destruct H2.
subst.
right; split; auto.
intros.
generalize dependent H2;
generalize dependent H3;
unfold substHeap; case Location_dec; intros.
subst.
generalize (searchClass_in_class _ _ _ H0); intros.
generalize (searchClass_in_class_nameClass _ _ _ H0); intros.
elim H1; rewrite (newObject_specif _ _ _ h1' H5 H6); auto.
auto.
Defined.
Index
This page has been generated by coqdoc