Library semantic
Require Export syntax.
Open Scope nat_scope.
Definition Location := positive.
Definition Location_dec := positive_dec.
Inductive Value : Set :=
| num : integer -> Value
| ref: Location -> Value
| null : Value.
Definition sem_binop : Operator -> integer -> integer -> integer :=
fun op =>
match op with
OpMult => mult
| OpPlus => plus
end.
Definition OperandStack := (list Value).
Definition LocalVar := Var -> Value.
Definition substLocalVar :
LocalVar -> Var -> Value -> LocalVar :=
fun L i0 v0 i =>
match (Var_dec i i0) with
| (left _) => v0
| (right _) => (L i)
end.
Record ClassInst : Set := classInstConstr{
class : ClassName;
fieldValue : FieldName -> Value
}.
Definition initField : typeOfField->Value :=
fun t=> match t with
| fieldNum => (num (O))
| fieldRef => null
end.
Definition def : Class -> ClassInst :=
fun c =>
(classInstConstr (nameClass c)
(fun (f:FieldName) =>
match (searchField c f) with
None => null
| (Some fi) => (initField (typeField fi))
end)).
Definition substField :
ClassInst -> FieldName -> Value -> ClassInst :=
fun o f0 v0 =>
(classInstConstr (class o)
(fun f => match (Field_dec f f0) with
| (left _) => v0
| (right _) => (fieldValue o f)
end)).
Lemma class_substField : forall o f v,
class (substField o f v) = class o.
unfold substField; intros; simpl; auto.
Qed.
Lemma fieldValue_substField1 : forall o f1 f2 v,
eq_word f2 f1 ->
fieldValue (substField o f1 v) f2 = v.
unfold substField; intros; simpl.
case Field_dec; intros.
reflexivity.
elim n; auto.
Qed.
Lemma fieldValue_substField2 : forall o f1 f2 v,
~eq_word f2 f1 ->
fieldValue (substField o f1 v) f2 = fieldValue o f2.
unfold substField; intros; simpl.
case Field_dec; intros.
elim H; auto.
reflexivity.
Qed.
Definition Heap := Location -> (option ClassInst).
Definition substHeap : Heap -> Location -> ClassInst -> Heap :=
fun H i0 v0 i =>
match (Location_dec i i0) with
| (left _) => (Some v0)
| (right _) => (H i)
end.
Axiom newObject : Program -> ClassName -> Heap -> Location.
Axiom newObject_specif : forall (P:Program) (c:Class) (cl:ClassName) (H:Heap),
(In c (classes P)) -> eq_word cl (nameClass c) ->
(H (newObject P cl H))= None.
Axiom newObject_same : forall P cl h1 h2,
(forall loc, h1 loc = None <-> h2 loc = None) ->
(newObject P cl h1) = (newObject P cl h2).
Inductive Frame : Set :=
| frame : MethodName -> progCount -> LocalVar -> OperandStack -> Frame.
Definition CallStack := (list Frame).
Inductive State : Set :=
| config : Heap -> progCount -> LocalVar -> OperandStack -> State.
Notation "<< h , pc , l , s >>" := (config h pc l s) (at level 0).
Inductive rule : Set :=
| nop1 : rule
| push1 : integer -> rule
| pop1 : rule
| numop1 : Operator -> rule
| load1 : Var -> rule
| store1 : Var -> rule
| If1 : progCount -> rule
| If2 : progCount -> rule
| new1 : ClassName -> rule
| putfield1 : FieldName -> rule
| getfield1 : FieldName -> rule
| goto1 : progCount -> rule.
Inductive SmallStepSem (P:Program) : rule -> State -> State -> Prop :=
| nop_rule : forall h pc l s,
instructionAt P pc=Some nop ->
SmallStepSem P nop1
<<h,pc,l,s>>
<<h,nextAddress P pc,l,s>>
| push_rule : forall h pc l s c,
instructionAt P pc=Some (push c) ->
SmallStepSem P (push1 c)
<<h,pc,l,s>>
<<h,nextAddress P pc,l,(num c)::s>>
| pop_rule : forall h pc l s v,
instructionAt P pc=Some pop ->
SmallStepSem P pop1
<<h,pc,l,v::s>>
<<h,nextAddress P pc,l,s>>
| numpop_rule : forall h pc l s op n1 n2,
instructionAt P pc=Some (numop op) ->
SmallStepSem P (numop1 op)
<<h,pc,l,(num n1)::(num n2)::s>>
<<h,nextAddress P pc,l,(num (sem_binop op n1 n2))::s>>
| load_rule : forall h pc l s x,
instructionAt P pc=Some (load x) ->
SmallStepSem P (load1 x)
<<h,pc,l,s>>
<<h,nextAddress P pc,l,(l x)::s>>
| store_rule : forall h pc l s x v,
instructionAt P pc=Some (store x) ->
SmallStepSem P (store1 x)
<<h,pc,l,v::s>>
<<h,nextAddress P pc,substLocalVar l x v,s>>
| if_not_nul_rule : forall h pc l s pc' n,
instructionAt P pc=Some (If pc') -> ~n=0 ->
SmallStepSem P (If1 pc')
<<h,pc,l,(num n)::s>>
<<h,pc',l,s>>
| if_nul_rule : forall h pc l s pc' n,
instructionAt P pc=Some (If pc') -> n=0 ->
SmallStepSem P (If2 pc')
<<h,pc,l,(num n)::s>>
<<h,nextAddress P pc,l,s>>
| goto_rule : forall h pc l s pc',
instructionAt P pc=Some (goto pc') ->
SmallStepSem P (goto1 pc')
<<h,pc,l,s>>
<<h,pc',l,s>>
| new_rule : forall h pc l s cl loc h' c,
instructionAt P pc=Some (new cl) ->
searchClass P cl=Some c ->
loc = newObject P cl h ->
h' = substHeap h loc (def c) ->
SmallStepSem P (new1 cl)
<<h,pc,l,s>>
<<h',nextAddress P pc,l,(ref loc)::s>>
| putfield_rule : forall h pc l s f v loc o,
instructionAt P pc=Some (putfield f) ->
h loc=Some o ->
In f (definedFields P (class o)) ->
SmallStepSem P (putfield1 f)
<<h,pc,l,v::(ref loc)::s>>
<<(substHeap h loc (substField o f v)),nextAddress P pc,l,s>>
| getfield_rule : forall h pc l s f loc o,
instructionAt P pc=Some (getfield f) ->
h loc=Some o ->
In f (definedFields P (class o)) ->
SmallStepSem P (getfield1 f)
<<h,pc,l,(ref loc)::s>>
<<h,nextAddress P pc,l,(fieldValue o f)::s>>.
Inductive SmallStepSem_star (P:Program): State -> State -> Prop :=
| SmallStepSem_star_0 : forall s, SmallStepSem_star P s s
| SmallStepSem_star_rec : forall i s1 s2 s3,
SmallStepSem_star P s1 s2 ->
SmallStepSem P i s2 s3 -> SmallStepSem_star P s1 s3.
Inductive Trace : Set :=
| Trace_init : State -> Trace
| Trace_next : State -> Trace -> Trace.
Coercion Trace_init : State >-> Trace.
Notation "l ::: s1" := (Trace_next s1 l) (at level 60).
Inductive initial_State (P:Program) : State -> Prop :=
init_State : forall (l:LocalVar),
(forall (x:Var), (l x)=null) ->
(initial_State P <<fun loc => None, Word_1 , l, nil >>).
Definition currentState : Trace -> State := fun tr =>
match tr with
Trace_init st => st
| Trace_next st _ => st
end.
Inductive in_tr (st:State) : Trace -> Prop :=
| in_tr_current : forall st' tr,
st=currentState tr -> in_tr st (tr:::st')
| in_tr_rest : forall st' tr,
in_tr st tr -> in_tr st (tr:::st').
Inductive SemCol' (P:Program) : Trace -> Prop :=
| SemCol_init : forall st, initial_State P st -> SemCol' P st
| SemCol_next : forall st tr i,
SemCol' P tr ->
SmallStepSem P i (currentState tr) st ->
SemCol' P (tr:::st).
Inductive SmallStepSemTrace (P:Program) (i:rule) : Trace -> Trace -> Prop :=
| SmallStepSemTrace_def : forall st tr,
SmallStepSem P i (currentState tr) st ->
SmallStepSemTrace P i tr (tr:::st).
Definition hSt (st:State) : Heap :=
let (h,_,_,_):=st in h.
Definition pcSt : State -> progCount := fun st =>
let (_,pc,_,_):=st in pc.
Definition valid_trace := SemCol'.
Definition VTrace := fun (P:Program) => {tr : Trace | valid_trace P tr}.
Definition vtr (P:Program) : VTrace P -> Trace := fun vtr =>
let (tr,_):=vtr in tr.
Coercion vtr : VTrace >-> Trace.
Lemma initial_state_valid : forall P st,
initial_State P st ->
valid_trace P st.
intros; auto.
constructor 1; auto.
Qed.
Definition valid_trace2 (P:Program) (tr:Trace) :=
forall st' loc o,
in_tr st' tr ->
(hSt st' loc)=Some o ->
~(hSt (currentState tr) loc)=None.
Lemma SemCol'_valid2 : forall P tr,
SemCol' P tr -> valid_trace2 P tr.
intros P tr H; unfold valid_trace2; intros.
generalize H1 H; clear H1 H; induction H0; intros; simpl.
inversion_clear H0.
rewrite <- H in H3; clear H.
inversion_clear H3 in H1; simpl in *; try (rewrite H1; discriminate).
subst.
unfold substHeap; case Location_dec; intros.
discriminate.
rewrite H1; discriminate.
unfold substHeap; case Location_dec; intros.
discriminate.
rewrite H1; discriminate.
inversion_clear H.
generalize (IHin_tr H1 H2).
CaseEq (currentState tr); intros h pc l s Heq; rewrite Heq in H3.
inversion_clear H3; simpl; auto; intros.
subst; unfold substHeap; case Location_dec; intros.
discriminate.
auto.
unfold substHeap; case Location_dec; intros.
discriminate.
auto.
Qed.
Definition valid_trace3 (P:Program) : Trace -> Prop := fun tr =>
forall st,
in_tr st tr ->
(forall cl, instructionAt P (pcSt st) = Some (new cl) ->
(exists c, searchClass P cl=Some c)).
Lemma SemCol'_valid3 : forall P tr,
SemCol' P tr -> valid_trace3 P tr.
intros P tr H; induction H; unfold valid_trace3; intros.
inversion_clear H0.
inversion_clear H1.
rewrite <- H3 in H0; destruct st0 as [h pc l s]; clear H3; simpl in H2.
inversion_clear H0; rewrite H1 in H2; try discriminate H2.
injection H2; intros H5'; injection H5'; intros; subst; eauto.
apply (IHSemCol' st0); auto.
Qed.
Definition rule2instr : rule -> Instruction := fun r =>
match r with
| nop1 => nop
| push1 c => push c
| pop1 => pop
| numop1 op => numop op
| load1 x => load x
| store1 x => store x
| If1 pc => If pc
| If2 pc => If pc
| new1 cl => new cl
| putfield1 f => putfield f
| getfield1 f => getfield f
| goto1 pc => goto pc
end.
Lemma invariant_instructionAt : forall P i h1 pc1 l1 s1 st2,
SmallStepSem P i << h1, pc1, l1, s1 >> st2 ->
instructionAt P pc1 = Some (rule2instr i).
intros.
inversion_clear H; simpl; assumption.
Qed.
Definition valid_trace4 (P:Program) : Trace -> Prop := fun tr =>
forall st,
in_tr st tr ->
exists st', exists r,
instructionAt P (pcSt st) = Some (rule2instr r)
/\ SmallStepSem P r st st'
/\ (st'=currentState tr \/ in_tr st' tr).
Lemma SemCol'_valid4 : forall P tr,
SemCol' P tr -> valid_trace4 P tr.
intros P tr H; induction H; unfold valid_trace4; intros.
inversion_clear H0.
inversion_clear H1.
rewrite <- H2 in H0.
exists st; exists i; split.
destruct st0; apply (invariant_instructionAt _ _ _ _ _ _ _ H0).
split; simpl; auto.
elim (IHSemCol' _ H2); intros st' (r,(H1,(H3,H4))).
exists st'; exists r; split; auto.
split; simpl; auto.
right; elim H4; clear H4; intros.
constructor 1; auto.
constructor 2; auto.
Qed.
Inductive secondState (st:State) : Trace -> Prop :=
secondState_def1 : forall st',
secondState st (st:::st')
| secondState_def2 : forall st' tr,
secondState st (tr:::st:::st').
Definition valid_trace1' (P:Program) (tr:Trace) : Prop :=
forall st' loc,
in_tr st' tr ->
(hSt (currentState tr) loc)=None ->
(hSt st' loc)=None.
Lemma SmallStepSem_null : forall P i st1 st2 loc,
SmallStepSem P i st1 st2 ->
hSt st2 loc = None ->
hSt st1 loc = None.
intros until 1.
inversion_clear H; simpl; auto.
subst; unfold substHeap; simpl; case Location_dec; intros.
discriminate H.
auto.
unfold substHeap; simpl; case Location_dec; intros.
discriminate H.
auto.
Qed.
Lemma SemCol'_valid1' : forall P tr,
SemCol' P tr -> valid_trace1' P tr.
unfold valid_trace1'.
induction tr; intros.
inversion_clear H0.
simpl in H1.
inversion_clear H0.
inversion_clear H.
rewrite <- H2 in H3.
apply (SmallStepSem_null P i st' s loc); auto.
inversion_clear H.
apply (IHtr H0 st'); auto.
apply (SmallStepSem_null P i (currentState tr) s loc); auto.
Qed.
Definition valid_trace1 (P:Program) (tr:Trace) : Prop :=
forall st st' cl cl',
in_tr st tr -> in_tr st' tr ->
instructionAt P (pcSt st) = Some (new cl) ->
instructionAt P (pcSt st') = Some (new cl') ->
(newObject P cl (hSt st))=(newObject P cl' (hSt st')) ->
st=st'.
Axiom SemCol'_valid1_temp : forall P st tr i st' st0 cl cl',
SemCol' P tr ->
SmallStepSem P i (currentState tr) st ->
in_tr st' (tr:::st) ->
instructionAt P (pcSt st0) = Some (new cl) ->
instructionAt P (pcSt st') = Some (new cl') ->
(newObject P cl (hSt st0))=(newObject P cl' (hSt st')) ->
st0 = currentState tr ->
st0=st'.
Lemma SemCol'_valid1 : forall P tr,
SemCol' P tr -> valid_trace1 P tr.
unfold valid_trace1; intros P tr Hsem.
induction Hsem; intros.
inversion_clear H0.
inversion_clear H0.
apply (SemCol'_valid1_temp P st tr i st' st0 cl cl'); auto.
inversion_clear H1.
rewrite (SemCol'_valid1_temp P st tr i st0 st' cl' cl); auto.
constructor 2; auto.
apply IHHsem with cl cl'; auto.
Qed.
Definition SemCol (P:Program) : VTrace P -> Prop := fun tr =>
SemCol' P tr.
Definition Context := {P:Program & VTrace P}.
Definition RelContext := Context -> Context -> Prop.
Definition VTR (P:Program) (tr:Trace) (H:valid_trace P tr) : VTrace P.
intros.
exists tr; auto.
Defined.
Definition Ct (P:Program) (tr:VTrace P) :=
(existS VTrace P tr).
Inductive SmallStepSemContext (i:rule) : Context -> Context -> Prop :=
SmallStepSemContext_def : forall P (tr1 tr2:VTrace P),
SmallStepSemTrace P i tr1 tr2 ->
SmallStepSemContext i (Ct P tr1) (Ct P tr2).
Inductive instr_not_new : rule -> Prop :=
| nop1_monotone_for_gammaHeap : instr_not_new nop1
| push1_monotone_for_gammaHeap : forall c, instr_not_new (push1 c)
| pop1_monotone_for_gammaHeap : instr_not_new pop1
| numop1_monotone_for_gammaHeap : forall op, instr_not_new (numop1 op)
| load1_monotone_for_gammaHeap : forall x, instr_not_new (load1 x)
| store1_monotone_for_gammaHeap : forall x, instr_not_new (store1 x)
| If1_monotone_for_gammaHeap : forall pc, instr_not_new (If1 pc)
| If2_monotone_for_gammaHeap : forall pc, instr_not_new (If2 pc)
| putfield1_monotone_for_gammaHeap : forall f, instr_not_new (putfield1 f)
| getfield1_monotone_for_gammaHeap : forall f, instr_not_new (getfield1 f)
| goto1_monotone_for_gammaHeap : forall pc,instr_not_new (goto1 pc).
Index
This page has been generated by coqdoc