14 describes correct typings of method bodies; it corresponds |
14 describes correct typings of method bodies; it corresponds |
15 to type \emph{checking}. |
15 to type \emph{checking}. |
16 \<close> |
16 \<close> |
17 |
17 |
18 definition |
18 definition |
19 \<comment> "The program counter will always be inside the method:" |
19 \<comment> \<open>The program counter will always be inside the method:\<close> |
20 check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool" where |
20 check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool" where |
21 "check_bounded ins et \<longleftrightarrow> |
21 "check_bounded ins et \<longleftrightarrow> |
22 (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and> |
22 (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and> |
23 (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)" |
23 (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)" |
24 |
24 |
25 definition |
25 definition |
26 \<comment> "The method type only contains declared classes:" |
26 \<comment> \<open>The method type only contains declared classes:\<close> |
27 check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where |
27 check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where |
28 "check_types G mxs mxr phi \<longleftrightarrow> set phi \<subseteq> states G mxs mxr" |
28 "check_types G mxs mxr phi \<longleftrightarrow> set phi \<subseteq> states G mxs mxr" |
29 |
29 |
30 definition |
30 definition |
31 \<comment> "An instruction is welltyped if it is applicable and its effect" |
31 \<comment> \<open>An instruction is welltyped if it is applicable and its effect\<close> |
32 \<comment> "is compatible with the type at all successor instructions:" |
32 \<comment> \<open>is compatible with the type at all successor instructions:\<close> |
33 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count, |
33 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count, |
34 exception_table,p_count] \<Rightarrow> bool" where |
34 exception_table,p_count] \<Rightarrow> bool" where |
35 "wt_instr i G rT phi mxs max_pc et pc \<longleftrightarrow> |
35 "wt_instr i G rT phi mxs max_pc et pc \<longleftrightarrow> |
36 app i G mxs rT pc et (phi!pc) \<and> |
36 app i G mxs rT pc et (phi!pc) \<and> |
37 (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')" |
37 (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')" |
41 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool" where |
41 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool" where |
42 "wt_start G C pTs mxl phi \<longleftrightarrow> |
42 "wt_start G C pTs mxl phi \<longleftrightarrow> |
43 G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" |
43 G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" |
44 |
44 |
45 definition |
45 definition |
46 \<comment> "A method is welltyped if the body is not empty, if execution does not" |
46 \<comment> \<open>A method is welltyped if the body is not empty, if execution does not\<close> |
47 \<comment> "leave the body, if the method type covers all instructions and mentions" |
47 \<comment> \<open>leave the body, if the method type covers all instructions and mentions\<close> |
48 \<comment> "declared classes only, if the method calling convention is respected, and" |
48 \<comment> \<open>declared classes only, if the method calling convention is respected, and\<close> |
49 \<comment> "if all instructions are welltyped." |
49 \<comment> \<open>if all instructions are welltyped.\<close> |
50 wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list, |
50 wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list, |
51 exception_table,method_type] \<Rightarrow> bool" where |
51 exception_table,method_type] \<Rightarrow> bool" where |
52 "wt_method G C pTs rT mxs mxl ins et phi \<longleftrightarrow> |
52 "wt_method G C pTs rT mxs mxl ins et phi \<longleftrightarrow> |
53 (let max_pc = length ins in |
53 (let max_pc = length ins in |
54 0 < max_pc \<and> |
54 0 < max_pc \<and> |
57 check_types G mxs (1+length pTs+mxl) (map OK phi) \<and> |
57 check_types G mxs (1+length pTs+mxl) (map OK phi) \<and> |
58 wt_start G C pTs mxl phi \<and> |
58 wt_start G C pTs mxl phi \<and> |
59 (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc))" |
59 (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc))" |
60 |
60 |
61 definition |
61 definition |
62 \<comment> "A program is welltyped if it is wellformed and all methods are welltyped" |
62 \<comment> \<open>A program is welltyped if it is wellformed and all methods are welltyped\<close> |
63 wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool" where |
63 wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool" where |
64 "wt_jvm_prog G phi \<longleftrightarrow> |
64 "wt_jvm_prog G phi \<longleftrightarrow> |
65 wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). |
65 wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). |
66 wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G" |
66 wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G" |
67 |
67 |