Library syntax
Require Export PosInf.
Require Export ZArith.
Require Export List.
Require Export FiniteSetLat.
Definition integer := nat.
Definition Var := Word.
Definition progCount := Word.
Definition Var_dec := eq_word_dec.
Definition ClassName := Word.
Definition FieldName := Word.
Definition Field_dec := eq_word_dec.
Definition MethodID := Word.
Definition MethodName := Word.
Definition MethodName_dec := eq_word_dec.
Inductive Operator : Set :=
| OpMult : Operator
| OpPlus : Operator.
Inductive ComponentType : Set :=
| NumericType : ComponentType
| ClassType : ClassName -> ComponentType.
Inductive Instruction : Set :=
| nop : Instruction
| push : integer -> Instruction
| push2 : integer -> Instruction
| pop : Instruction
| numop : Operator -> Instruction
| load : Var -> Instruction
| store : Var -> Instruction
| If : progCount -> Instruction
| new_o : ClassName -> Instruction
| putfield : FieldName -> Instruction
| getfield : FieldName -> Instruction
| goto : progCount -> Instruction
| new_a : ComponentType -> Instruction
| arraylength : Instruction
| arrayload : Instruction
| arraystore : Instruction
| invokevirtual : MethodID -> Instruction
| return_v : Instruction.
Inductive typeOfField : Set :=
| fieldNum : typeOfField
| fieldRef : typeOfField.
Record Field : Set := Field_constr {
nameField : FieldName;
typeField : typeOfField
}.
Definition nat2pos : nat -> positive := P_of_succ_nat.
Record Method : Set := Method_constr {
nameMethod : MethodName;
instructions : (list Instruction);
instructions_nb : inf_log (nat2pos (length instructions)) WordSize;
nbArguments : nat
}.
Inductive Methods_all_distinct : (list Method) -> Prop :=
Methods_all_distinct_nil : Methods_all_distinct nil
| Methods_all_distinct_cons : forall M l,
(forall M', In M' l -> ~ eq_word (nameMethod M) (nameMethod M')) ->
Methods_all_distinct l ->
Methods_all_distinct (M::l).
Record Class : Set := Class_constr {
nameClass : ClassName;
list_methods_lookup : (list (MethodID*MethodName));
instanceFields : (list Field)
}.
Record Program : Set := Program_constr {
classes : (list Class);
methods : (list Method);
main : Method;
methods_distincts : Methods_all_distinct (main::methods)
}.
Definition nth_positive := fun (l:(list Instruction)) (pc:positive) =>
nth_error l (pred (nat_of_P pc)).
Fixpoint searchMethod_rec (m0:MethodName) (l:(list Method)){struct l} : (option Method):=
match l with
nil => None
| (cons m q) =>
match (MethodName_dec m0 (nameMethod m)) with
| (left _) => (Some m)
| (right _) => (searchMethod_rec m0 q)
end
end.
Definition searchMethod := fun (P:Program) (m:MethodName) =>
(searchMethod_rec m (cons (main P) (methods P))).
Lemma searchMethod_eq_some : forall P M,
In M (main P :: methods P) ->
searchMethod P (nameMethod M) = Some M.
Proof.
unfold searchMethod; intros P M.
generalize (methods_distincts P).
generalize (main P :: methods P); intros l.
induction l; simpl; intros.
elim H0.
destruct H0.
subst; case MethodName_dec; intros; auto.
elim n; auto.
case MethodName_dec; intros; auto.
inversion_clear H.
elim (H1 _ H0).
apply eq_word_sym; auto.
inversion_clear H; auto.
Qed.
Lemma searchMethod_some : forall P m M,
searchMethod P m = Some M -> eq_word m (nameMethod M).
unfold searchMethod.
intros P m M.
generalize (main P :: methods P).
induction l; simpl; intros.
discriminate H.
generalize H; clear H; case (MethodName_dec m (nameMethod a)); intros.
injection H; clear H; intros; subst; auto.
auto.
Qed.
Lemma searchMethod_some_in : forall P m M,
searchMethod P m = Some M -> In M (main P :: methods P).
unfold searchMethod.
intros P m M.
generalize (main P :: methods P).
induction l; simpl; intros.
discriminate H.
generalize H; clear H; case (MethodName_dec m (nameMethod a)); intros.
injection H; clear H; intros; subst; auto.
auto.
Qed.
Definition instructionAt := fun (P:Program) (m:MethodName) (pc:progCount) =>
match (searchMethod P m) with
| None => None
| Some M => nth_positive (instructions M) (word2pos pc)
end.
Lemma searchMethod_rec_eq_word : forall m1 m2 l,
eq_word m1 m2 ->
searchMethod_rec m1 l = searchMethod_rec m2 l.
induction l; simpl; intros.
auto.
case (MethodName_dec m1 (nameMethod a)); intros.
case (MethodName_dec m2 (nameMethod a)); intros.
auto.
elim n; apply eq_word_trans with m1; auto.
case (MethodName_dec m2 (nameMethod a)); intros.
elim n; apply eq_word_trans with m2; auto.
auto.
Qed.
Lemma instructionAt_eq_word : forall P m1 m2 pc1 pc2,
eq_word m1 m2 ->
eq_word pc1 pc2 ->
(instructionAt P m1 pc1)=(instructionAt P m2 pc2).
unfold instructionAt; intros.
unfold searchMethod.
rewrite (searchMethod_rec_eq_word _ _ (main P :: methods P) H).
case (searchMethod_rec m2 (main P :: methods P)); intros; auto.
unfold nth_positive.
destruct pc1; destruct pc2; simpl in *.
subst; auto.
Qed.
Lemma instructionAt_in_methods : forall P m pc i,
instructionAt P m pc = Some i ->
exists M, In M (main P :: methods P) /\ eq_word m (nameMethod M).
unfold instructionAt.
intros P m pc i; CaseEq (searchMethod P m); intros.
generalize (searchMethod_some _ _ _ H); intros.
generalize (searchMethod_some_in _ _ _ H); intros.
eauto.
discriminate H0.
Qed.
Definition nextAddress : Program -> progCount -> progCount :=
fun P pc => (succ_word pc).
Lemma nextAddress_eq_word : forall P p1 p2,
eq_word p1 p2 ->
eq_word (nextAddress P p1) (nextAddress P p2).
unfold nextAddress; intros.
apply (PosInf.succ_word_eq_word _ _ H).
Qed.
Fixpoint searchField_rec (l:(list Field)) : FieldName->(option Field) :=
fun f => match l with
nil => None
| (cons fi q) => match (eq_word_dec f (nameField fi)) with
(left _) => (Some fi)
| (right _) => (searchField_rec q f)
end
end.
Definition searchField : Class->FieldName->(option Field) :=
fun c f => (searchField_rec (instanceFields c) f).
Fixpoint searchClass_rec (l:(list Class)) : ClassName->(option Class) :=
fun f => match l with
nil => None
| (cons fi q) => match (eq_word_dec f (nameClass fi)) with
(left _) => (Some fi)
| (right _) => (searchClass_rec q f)
end
end.
Lemma searchClass_rec_in_l : forall l cl c,
searchClass_rec l cl = Some c -> In c l.
induction l; simpl.
intros _ c H; inversion H.
intros cl c; case eq_word_dec; intros.
left; injection H; auto.
right; apply (IHl cl); auto.
Qed.
Lemma searchClass_rec_in_l_classname : forall l cl c,
searchClass_rec l cl = Some c -> eq_word cl (nameClass c).
induction l; simpl.
intros cl c H; inversion H.
intros cl c; case eq_word_dec; intros.
injection H; intros H1; rewrite <- H1; auto.
apply IHl; auto.
Qed.
Definition searchClass : Program->ClassName->(option Class) :=
fun P f => (searchClass_rec (classes P) f).
Lemma searchClass_in_class : forall P cl c,
searchClass P cl = Some c -> In c (classes P).
intros; apply searchClass_rec_in_l with cl; auto.
Qed.
Lemma searchClass_in_class_nameClass : forall P cl c,
searchClass P cl = Some c -> eq_word cl (nameClass c).
intros; apply searchClass_rec_in_l_classname with (classes P); auto.
Qed.
Lemma searchClass_eq_word : forall P cl1 cl2,
eq_word cl1 cl2 ->
searchClass P cl1 = searchClass P cl2.
unfold searchClass.
intros P cl1 cl2; generalize (classes P).
induction l; simpl; intros; auto.
case eq_word_dec; intros.
case eq_word_dec; intros.
auto.
elim n.
generalize dependent (nameClass a); intros.
destruct cl1; destruct cl2; destruct c; simpl in *; subst; auto.
case eq_word_dec; intros.
elim n.
generalize dependent (nameClass a); intros.
destruct cl1; destruct cl2; destruct c; simpl in *; subst; auto.
auto.
Qed.
Definition definedFields (P:Program) (cl:ClassName) : list FieldName :=
match (searchClass P cl) with
| Some c => map nameField (instanceFields c)
| None => nil
end.
Lemma definedFields_eq_word : forall P cl1 cl2,
eq_word cl1 cl2 ->
definedFields P cl1 = definedFields P cl2.
unfold definedFields; intros.
rewrite (searchClass_eq_word P cl1 cl2); auto.
Qed.
Lemma in_definedFields : forall P cl f,
In f (definedFields P cl) ->
exists c, searchClass P cl = Some c /\ ~ searchField c f = None /\
exists fi, In fi (instanceFields c) /\
f = nameField fi.
intros P cl f.
unfold definedFields.
CaseEq (searchClass P cl); intros.
exists c; split; auto.
split.
unfold searchField.
generalize dependent (instanceFields c).
induction l; simpl; intros.
elim H0.
elim H0; intros.
case eq_word_dec; intros.
discriminate.
elim n; rewrite H1.
destruct f; simpl; auto.
case eq_word_dec; intros.
discriminate.
auto.
generalize dependent (instanceFields c).
induction l; simpl; intros.
elim H0.
elim H0; intros.
eauto.
elim (IHl H1); intros.
exists x; intuition.
elim H0.
Qed.
Fixpoint searchWithMethodID (l:(list (MethodID*MethodName))) : MethodID->(option MethodName) :=
fun id0 => match l with
nil => None
| (cons (id,m) q) => match (eq_word_dec id0 id) with
(left _) => (Some m)
| (right _) => (searchWithMethodID q id0)
end
end.
Definition methodLookup : Program -> MethodID -> ClassName -> (option Method) :=
fun P id cl =>
match (searchClass P cl) with
None => None
|(Some c) => match (searchWithMethodID (list_methods_lookup c) id) with
None => None
|(Some m) => match (searchMethod P m) with
None => None
|(Some M) => (Some M)
end
end
end.
Lemma methodLookup_some_in : forall P mID cl M,
methodLookup P mID cl = Some M ->
In M ((main P)::(methods P)).
intros P mID cl M; unfold methodLookup.
CaseEq (searchClass P cl).
intros c H.
CaseEq (searchWithMethodID (list_methods_lookup c) mID).
intros m H1.
CaseEq (searchMethod P m); intros.
injection H2; intros; subst.
apply searchMethod_some_in with m; auto.
discriminate H2.
intros _ H2; discriminate H2.
intros _ H2; discriminate H2.
Qed.
Lemma methodLookup_some : forall P mID cl M,
methodLookup P mID cl = Some M ->
exists c, In c (classes P) /\
exists m', searchWithMethodID (list_methods_lookup c) mID = Some m'
/\ eq_word m' (nameMethod M).
intros P mID cl M; unfold methodLookup.
CaseEq (searchClass P cl).
intros c H.
CaseEq (searchWithMethodID (list_methods_lookup c) mID).
intros m H1.
CaseEq (searchMethod P m); intros.
exists c.
generalize (searchClass_in_class _ _ _ H); intros; split; auto.
rewrite H1.
exists m; split; auto.
injection H2; clear H2; intros; subst.
apply searchMethod_some with P; auto.
discriminate H2.
intros _ H2; discriminate H2.
intros _ H2; discriminate H2.
Qed.
Fixpoint implem_rec (mID:MethodID) (s:list MethodName) (l:list Class) {struct l} : list MethodName :=
match l with
| nil => s
| cons c q =>
match (searchWithMethodID (list_methods_lookup c) mID) with
| None => implem_rec mID s q
| Some m => implem_rec mID (m::s) q
end
end.
Definition implem (P:Program) (mID:MethodID) : list MethodName :=
implem_rec mID nil (classes P).
Lemma in_set_implem_rec : forall mID l m s,
In m s ->
In m (implem_rec mID s l).
induction l; simpl; intros; auto.
case (searchWithMethodID (list_methods_lookup a) mID); intros; auto.
apply IHl.
right; auto.
Qed.
Lemma methodLookup_in_implem : forall P mID cl M,
methodLookup P mID cl = Some M ->
exists m, In m (implem P mID) /\ eq_word m (nameMethod M).
intros.
elim (methodLookup_some _ _ _ _ H); clear H; intros c (H,(m,(H1,H2))).
generalize H; clear H; unfold implem.
generalize (nil (A:=MethodName)).
generalize (classes P).
induction l; simpl; intros.
elim H.
elim H; clear H; intros.
subst.
rewrite H1.
exists m; split; auto.
apply in_set_implem_rec.
left; auto.
CaseEq (searchWithMethodID (list_methods_lookup a) mID); intros; auto.
Qed.
Index
This page has been generated by coqdoc