186 "wt_start G C pTs mxl phi \\<equiv> |
186 "wt_start G C pTs mxl phi \\<equiv> |
187 G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0" |
187 G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0" |
188 |
188 |
189 |
189 |
190 wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool" |
190 wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool" |
191 "wt_method G cn pTs rT mxl ins phi \\<equiv> |
191 "wt_method G C pTs rT mxl ins phi \\<equiv> |
192 let max_pc = length ins |
192 let max_pc = length ins |
193 in |
193 in |
194 0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and> |
194 0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and> |
195 (\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)" |
195 (\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)" |
196 |
196 |
197 wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool" |
197 wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool" |
198 "wt_jvm_prog G phi \\<equiv> |
198 "wt_jvm_prog G phi \\<equiv> |
199 wf_prog (\\<lambda>G C (sig,rT,maxl,b). |
199 wf_prog (\\<lambda>G C (sig,rT,maxl,b). |