Library ObjectAlgebraImplem_struct
Require Export AlgebraType.
Definition gammaObjectPointWise : forall (P:Program) (V:Set) (PV:Lattice V),
Gamma (PowPoset Value) PV -> Gamma (PowPoset ClassInst) (ArrayLattice PV WordSize).
intros P V PV g.
refine (gamma_constr _ _
(fun O o => forall x,
In x (definedFields P (class o)) ->
(g (applyArray PV O x) (fieldValue o x))) _).
intros.
intros o H1 x H2.
apply (gamma_monotone g (applyArray PV b1 x)); auto.
apply applyArray_monotone; auto.
Defined.
Implicit Arguments gammaObjectPointWise [V].
Definition gammaTopObjectPointWise : forall (P:Program) (V:Set) (PV:Lattice V),
GammaTop (PowPoset Value) PV -> GammaTop (PowPoset ClassInst) (ArrayLattice PV WordSize).
intros P V PV g.
refine (gammatop_constr
(gammaObjectPointWise P PV g) _).
simpl; intros.
apply (gamma_top g (fun _ => True)); auto.
Defined.
Implicit Arguments gammaTopObjectPointWise [V].
Definition betaTypeOfField : forall (V:Set), V -> V ->
typeOfField -> V := fun V AbZero AbNull t =>
match t with
| fieldNum => AbZero
| fieldRef => AbNull
end.
Fixpoint AbDef_rec (V:Set) (PV:Lattice V)
(AbZero AbNull:V) (l:(list Field)) {struct l}: (funcTree' V WordSize) :=
match l with
nil => (bottom (ArrayLattice PV WordSize))
| (cons fi q) => (substArray PV (AbDef_rec V PV AbZero AbNull q) (nameField fi) (betaTypeOfField V AbZero AbNull (typeField fi)))
end.
Lemma betaTypeOfField_correct : forall (V:Set) (PV:Lattice V) (AbZero AbNull:V)
(g:Gamma (PowPoset Value) PV) fi,
(fun v => v = null) <=< (g AbNull) ->
(fun v => v = num (0)) <=< (g AbZero) ->
g (betaTypeOfField V AbZero AbNull (typeField fi))
(initField (typeField fi)).
Proof.
intros.
destruct (typeField fi); simpl; auto.
Qed.
Lemma AbDef_rec_correct : forall (V:Set) (PV:Lattice V) (AbZero AbNull:V)
(g:Gamma (PowPoset Value) PV)
(P:Program) (c:Class) (l:(list Field)) (f:FieldName) fi,
(In c (classes P)) ->
(incl l (instanceFields c)) ->
(searchField_rec l f)=(Some fi) ->
(fun v => v = null) <=< (g AbNull) ->
(fun v => v = num (0)) <=< (g AbZero) ->
(g (applyArray PV (AbDef_rec V PV AbZero AbNull l) f)
(initField (typeField fi))).
induction l; intros; simpl.
discriminate H1.
generalize H1; clear H1; simpl.
case eq_word_dec; intros.
injection H1; clear H1; intros; subst.
apply (gamma_monotone g (betaTypeOfField V AbZero AbNull (typeField fi))).
apply apply_substArray1; auto.
destruct f; destruct (nameField fi); simpl in *; auto.
apply betaTypeOfField_correct; auto.
rewrite apply_substArray2; auto.
apply IHl; auto.
intros x H'.
apply H0.
right; auto.
Qed.
Definition AbDef (V:Set) (PV:Lattice V) (AbZero AbNull:V)
(P:Program) (cl:ClassName) : (funcTree' V WordSize) :=
match (searchClass P cl) with
| None => (bottom (ArrayLattice PV WordSize))
| (Some c) => (AbDef_rec V PV AbZero AbNull (instanceFields c))
end.
Implicit Arguments AbDef [V].
Lemma AbDef_correct : forall (V:Set) (PV:Lattice V) (AbZero AbNull:V)
(g:Gamma (PowPoset Value) PV)
(P:Program) (cl:ClassName) c,
(fun v => v = null) <=< (g AbNull) ->
(fun v => v = num (0)) <=< (g AbZero) ->
searchClass P cl=Some c ->
gamma_func (gammaObjectPointWise P PV g) (AbDef PV AbZero AbNull P cl) (def c).
intros.
intros f; unfold def, AbDef.
rewrite H1; simpl.
intros H2.
CaseEq (searchField c f); intros.
apply AbDef_rec_correct with P c; auto.
apply searchClass_in_class with cl; auto.
intros x; auto.
elim (in_definedFields P cl f).
intros c' (H2',(H5,(fi,(H3',H4)))).
rewrite H2' in H1; injection H1; intros; subst.
elim H5; auto.
generalize (searchClass_in_class_nameClass _ _ _ H1); intros.
rewrite (definedFields_eq_word P cl (nameClass c)); auto.
Qed.
Definition ObjectAlgebra : forall (V:Set) (PV:Lattice V),
Object.Connect PV.
intros.
refine (Object.Build_Connect
(fun P => @gammaTopObjectPointWise P _ PV) _
(fun f o => applyArray PV o f) _
(fun f o v => substArray PV o f v) _
(fun P cl AbZero AbNull => (AbDef PV AbZero AbNull P cl)) _
).
intros P g1 g2 H O o H1 f Hf.
apply H; auto.
intros.
intros v H.
inversion_clear H.
inversion_clear H0 in H1.
apply H1; auto.
intros.
intros o' H f' H1.
inversion_clear H in H1.
inversion_clear H0 in H2 H3 H1.
unfold substField; simpl; case Field_dec; intros.
apply (gamma_monotone g v); auto.
apply apply_substArray1; auto.
destruct f; destruct f'; simpl; auto.
rewrite apply_substArray2; auto.
intros.
intros o H'.
inversion_clear H'.
inversion_clear H1.
apply (AbDef_correct V PV AbZero AbNull g P cl c); auto.
Qed.
Implicit Arguments ObjectAlgebra [V].
Index
This page has been generated by coqdoc