146 G \\<turnstile> (ST , LT) <=s phi ! (nat(int pc+branch)))" |
146 G \\<turnstile> (ST , LT) <=s phi ! (nat(int pc+branch)))" |
147 |
147 |
148 consts |
148 consts |
149 wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
149 wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
150 primrec |
150 primrec |
151 "wt_MI (Invokevirtual mn fpTs) G phi max_pc pc = |
151 "wt_MI (Invoke mn fpTs) G phi max_pc pc = |
152 (let (ST,LT) = phi ! pc |
152 (let (ST,LT) = phi ! pc |
153 in |
153 in |
154 pc+1 < max_pc \\<and> |
154 pc+1 < max_pc \\<and> |
155 (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and> |
155 (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and> |
156 length apTs = length fpTs \\<and> |
156 length apTs = length fpTs \\<and> |
157 (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and> |
157 (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and> |
158 (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and> |
158 (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and> |
159 G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))" |
159 G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))" |
160 |
160 |
161 constdefs |
161 consts |
162 wt_MR :: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool" |
162 wt_MR :: "[meth_ret,jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool" |
163 "wt_MR G rT phi pc \\<equiv> |
163 primrec |
|
164 "wt_MR Return G rT phi pc = |
164 (let (ST,LT) = phi ! pc |
165 (let (ST,LT) = phi ! pc |
165 in |
166 in |
166 (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))" |
167 (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))" |
167 |
168 |
168 |
169 |
173 LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc |
174 LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc |
174 | CO ins \\<Rightarrow> wt_CO ins G phi max_pc pc |
175 | CO ins \\<Rightarrow> wt_CO ins G phi max_pc pc |
175 | MO ins \\<Rightarrow> wt_MO ins G phi max_pc pc |
176 | MO ins \\<Rightarrow> wt_MO ins G phi max_pc pc |
176 | CH ins \\<Rightarrow> wt_CH ins G phi max_pc pc |
177 | CH ins \\<Rightarrow> wt_CH ins G phi max_pc pc |
177 | MI ins \\<Rightarrow> wt_MI ins G phi max_pc pc |
178 | MI ins \\<Rightarrow> wt_MI ins G phi max_pc pc |
178 | MR \\<Rightarrow> wt_MR G rT phi pc |
179 | MR ins \\<Rightarrow> wt_MR ins G rT phi pc |
179 | OS ins \\<Rightarrow> wt_OS ins G phi max_pc pc |
180 | OS ins \\<Rightarrow> wt_OS ins G phi max_pc pc |
180 | BR ins \\<Rightarrow> wt_BR ins G phi max_pc pc" |
181 | BR ins \\<Rightarrow> wt_BR ins G phi max_pc pc" |
181 |
182 |
182 |
183 |
183 constdefs |
184 constdefs |