Library RefAlgebraImplem_point
Require Export AlgebraType.
Section P.
Variable P : Program.
Definition PfPt := FiniteSet WordSize.
Definition RelPt : VTrace P -> VTrace P -> Prop :=
fun tr1 tr2 =>
forall st cl,
in_tr st tr1 ->
instructionAt P (pcSt st) = Some (new cl) ->
in_tr st tr2.
Definition gammaPt (tr:VTrace P) (s:PfPt) (loc:Location) : Prop :=
s = None \/
exists st,
(in_set (pcSt st) s = true) /\
(in_tr st tr) /\
exists cl, instructionAt P (pcSt st) = Some (new cl) /\
loc = newObject P cl (hSt st).
Definition gammaRefPt : VTrace P -> Gamma (PowPoset Location) (LatticeFiniteSet WordSize).
intros tr.
refine (gamma_constr (PowPoset Location) (LatticeFiniteSet WordSize)
(gammaPt tr)
_).
intros b1 b2 H loc.
inversion_clear H; intros.
left; auto.
destruct H.
discriminate H.
destruct H as [st (H1,(H2,(cl,(H3,H4))))].
right; exists st; repeat split; auto.
apply in_set_monotone with (Some f1); auto.
constructor; auto.
eauto.
Defined.
Definition gammaTopRefPt : VTrace P -> GammaTop (PowPoset Location) (LatticeFiniteSet WordSize).
intros tr.
refine (gammatop_constr (gammaRefPt tr) _).
simpl; intros; left; auto.
Defined.
Definition gammaBestTopRefPt : VTrace P -> GammaBestTop Location LatticeAtomFiniteSet.
intros tr.
refine (gammabesttop_constr LatticeAtomFiniteSet (gammaTopRefPt tr) _ _).
simpl; intros.
destruct b; auto.
destruct H0.
discriminate H0.
destruct H0 as [st (H1,(H2,(cl,(H3,H4))))].
destruct H.
discriminate H.
destruct H as [st' (H1',(H2',(cl',(H3',H4'))))].
assert (valid_trace1 P tr).
apply SemCol'_valid1; destruct tr; auto.
rewrite <- (H st st' cl cl') in H1'; auto.
apply in_set_eq with (pcSt st); auto.
apply in_set_singleton; auto.
subst; auto.
simpl; intros.
destruct H.
intuition.
destruct H as [st (H1,(H2,(cl,(H3,H4))))].
exists (pcSt st).
right.
exists st; intuition.
apply in_singleton.
eauto.
Defined.
Definition RefAlgebraPt : Ref.Connect P.
refine (Ref.Build_Connect
RelPt
(fun tr => tr)
gammaBestTopRefPt _
(fun cl pc => (singleton pc)) _ _ _ _).
intros tr1 tr2 H s loc H1.
destruct H1.
left; auto.
destruct H0 as [st (H1,(H2,(cl,(H3,H4))))].
right; exists st; repeat split; eauto.
intros (tr1,Htr1) (tr2,Htr2) cl pc Hsem H loc H1; simpl in *.
inversion_clear H1.
inversion_clear H0.
unfold gammaPt; simpl in_tr.
inversion_clear Hsem.
CaseEq (currentState tr1); intros.
rewrite H4 in H; rewrite H4 in H2; rewrite H4 in H0; subst.
inversion_clear H0.
right.
exists (<< h, p, l, o >>); repeat split.
simpl pcSt.
apply in_singleton.
constructor 1; auto.
exists cl; split; auto.
intros (tr1,H1) (tr2,H2) r H.
intros st' cl; simpl in *.
inversion_clear H; intros.
constructor 2 ;auto.
intros (tr1,H1) (tr2,H2) r H H' st cl; simpl in *.
inversion_clear H in H'; intros.
inversion_clear H; auto.
subst.
CaseEq (currentState tr1); intros h1 pc1 l1 s1 Heq.
rewrite Heq in H3; rewrite Heq in H0; clear Heq; simpl in *.
inversion_clear H0 in H'; try (rewrite H in H3; discriminate H3).
inversion_clear H'.
intros cl (tr1,H1) (tr2,H2) h R loc Hsem H4 H5 H3; simpl in *.
destruct H3.
left; auto.
right; simpl in_tr in *.
destruct H as [st (H6,(H7,(cl',(H8,H9))))].
exists st; repeat split; eauto.
inversion_clear Hsem in H7.
inversion_clear H7; auto.
subst.
CaseEq (currentState tr1); intros h1 pc1 l1 s1 Heq.
rewrite Heq in H6; rewrite Heq in H5; rewrite Heq in H; rewrite Heq in H8;
clear Heq; simpl in *.
inversion_clear H.
generalize (searchClass_in_class_nameClass _ _ _ H3); intros.
generalize (searchClass_in_class _ _ _ H3); intros.
rewrite H8 in H0; injection H0; intros; subst.
rewrite (newObject_specif P _ _ h1 H9 H) in H5.
elim H5; auto.
Defined.
End P.
Index
This page has been generated by coqdoc