text\<open>
This theorycontains a specification of the BV. The specification
describes correct typings of method bodies; it corresponds to type \emph{checking}. \<close>
definition \<comment> \<open>The program counter will always be inside the method:\<close>
check_bounded :: "instr list \ exception_table \ bool" where "check_bounded ins et \
(\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
(\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
definition \<comment> \<open>The method type only contains declared classes:\<close>
check_types :: "jvm_prog \ nat \ nat \ JVMType.state list \ bool" where "check_types G mxs mxr phi \ set phi \ states G mxs mxr"
definition \<comment> \<open>An instruction is welltyped if it is applicable and its effect\<close> \<comment> \<open>is compatible with the type at all successor instructions:\<close>
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
exception_table,p_count] \<Rightarrow> bool" where "wt_instr i G rT phi mxs max_pc et pc \
app i G mxs rT pc et (phi!pc) \<and>
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
definition \<comment> \<open>The type at \<open>pc=0\<close> conforms to the method calling convention:\<close>
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \ bool" where "wt_start G C pTs mxl phi \
G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
definition \<comment> \<open>A method is welltyped if the body is not empty, if execution does not\<close> \<comment> \<open>leave the body, if the method type covers all instructions and mentions\<close> \<comment> \<open>declared classes only, if the method calling convention is respected, and\<close> \<comment> \<open>if all instructions are welltyped.\<close>
wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
exception_table,method_type] \<Rightarrow> bool" where "wt_method G C pTs rT mxs mxl ins et phi \
(let max_pc = length ins in
0 < max_pc \<and>
length phi = length ins \<and>
check_bounded ins et \<and>
check_types G mxs (1+length pTs+mxl) (map OK phi) \<and>
wt_start G C pTs mxl phi \<and>
(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc))"
definition \<comment> \<open>A program is welltyped if it is wellformed and all methods are welltyped\<close>
wt_jvm_prog :: "[jvm_prog,prog_type] \ bool" where "wt_jvm_prog G phi \
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
lemma wt_jvm_progD: "wt_jvm_prog G phi \ (\wt. wf_prog wt G)" by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr: "\ wt_jvm_prog G phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins \<rbrakk> \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
text\<open>
We could leave out the check \<^term>\<open>pc' < max_pc\<close> in the definition of \<^term>\<open>wt_instr\<close> in the context of \<^term>\<open>wt_method\<close>. \<close> lemma wt_instr_def2: "\ wt_jvm_prog G Phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins;
i = ins!pc; phi = Phi C sig; max_pc = length ins \<rbrakk> \<Longrightarrow> wt_instr i G rT phi maxs max_pc et pc =
(app i G maxs rT pc et (phi!pc) \<and>
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). G \<turnstile> s' <=' phi!pc'))" apply (simp add: wt_instr_def) apply (unfold wt_jvm_prog_def) apply (drule method_wf_mdecl) apply (simp, simp, simp add: wf_mdecl_def wt_method_def) apply (auto dest: check_boundedD) done
lemma wt_jvm_prog_impl_wt_start: "\ wt_jvm_prog G phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<rbrakk> \<Longrightarrow>
0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)" by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
