1.1 --- a/src/HOL/MicroJava/BV/BVSpec.ML Wed Nov 24 13:36:14 1999 +0100
1.2 +++ b/src/HOL/MicroJava/BV/BVSpec.ML Thu Nov 25 12:01:28 1999 +0100
1.3 @@ -4,8 +4,6 @@
1.4 Copyright 1999 Technische Universitaet Muenchen
1.5 *)
1.6
1.7 -Addsimps [wt_MR_def];
1.8 -
1.9 Goalw [wt_jvm_prog_def] "wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)";
1.10 by(Blast_tac 1);
1.11 qed "wt_jvm_progD";
2.1 --- a/src/HOL/MicroJava/BV/BVSpec.thy Wed Nov 24 13:36:14 1999 +0100
2.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 25 12:01:28 1999 +0100
2.3 @@ -148,7 +148,7 @@
2.4 consts
2.5 wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
2.6 primrec
2.7 -"wt_MI (Invokevirtual mn fpTs) G phi max_pc pc =
2.8 +"wt_MI (Invoke mn fpTs) G phi max_pc pc =
2.9 (let (ST,LT) = phi ! pc
2.10 in
2.11 pc+1 < max_pc \\<and>
2.12 @@ -158,9 +158,10 @@
2.13 (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
2.14 G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
2.15
2.16 -constdefs
2.17 - wt_MR :: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
2.18 -"wt_MR G rT phi pc \\<equiv>
2.19 +consts
2.20 + wt_MR :: "[meth_ret,jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
2.21 +primrec
2.22 + "wt_MR Return G rT phi pc =
2.23 (let (ST,LT) = phi ! pc
2.24 in
2.25 (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
2.26 @@ -175,7 +176,7 @@
2.27 | MO ins \\<Rightarrow> wt_MO ins G phi max_pc pc
2.28 | CH ins \\<Rightarrow> wt_CH ins G phi max_pc pc
2.29 | MI ins \\<Rightarrow> wt_MI ins G phi max_pc pc
2.30 - | MR \\<Rightarrow> wt_MR G rT phi pc
2.31 + | MR ins \\<Rightarrow> wt_MR ins G rT phi pc
2.32 | OS ins \\<Rightarrow> wt_OS ins G phi max_pc pc
2.33 | BR ins \\<Rightarrow> wt_BR ins G phi max_pc pc"
2.34
3.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Wed Nov 24 13:36:14 1999 +0100
3.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 25 12:01:28 1999 +0100
3.3 @@ -10,7 +10,7 @@
3.4 Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
3.5 "\\<lbrakk> wt_jvm_prog G phi; \
3.6 \ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
3.7 -\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
3.8 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
3.9 \\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
3.10 by (Asm_full_simp_tac 1);
3.11 by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1);
3.12 @@ -28,8 +28,8 @@
3.13 \ ins!pc = LS(Load idx); \
3.14 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.15 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.16 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.17 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.18 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.19 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.20 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
3.21 approx_loc_imp_approx_loc_sup]
3.22 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.23 @@ -42,8 +42,8 @@
3.24 \ ins!pc = LS(Store idx); \
3.25 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.26 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.27 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.28 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.29 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.30 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.31 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.32 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]
3.33 addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.34 @@ -60,8 +60,8 @@
3.35 \ ins!pc = LS(Bipush i); \
3.36 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.37 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.38 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.39 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.40 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.41 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.42 by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
3.43 addss (simpset() addsimps [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
3.44 qed "Bipush_correct";
3.45 @@ -84,8 +84,8 @@
3.46 \ ins!pc = LS Aconst_null; \
3.47 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.48 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.49 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.50 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.51 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.52 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.53 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
3.54 addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
3.55 qed "Aconst_null_correct";
3.56 @@ -96,8 +96,8 @@
3.57 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.58 \ ins!pc = LS ls_com; \
3.59 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.60 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.61 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.62 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.63 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.64 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.65 ba 1;
3.66 ba 1;
3.67 @@ -131,8 +131,8 @@
3.68 \ ins!pc = CH (Checkcast D); \
3.69 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.70 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.71 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.72 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.73 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.74 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.75 by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,
3.76 xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.77 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.78 @@ -146,8 +146,8 @@
3.79 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.80 \ ins!pc = CH ch_com; \
3.81 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.82 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.83 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.84 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.85 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.86 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.87 ba 1;
3.88 ba 1;
3.89 @@ -164,8 +164,8 @@
3.90 \ ins!pc = MO (Getfield F D); \
3.91 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.92 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.93 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.94 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.95 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.96 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.97 by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.98 by (Clarify_tac 1);
3.99 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
3.100 @@ -203,8 +203,8 @@
3.101 \ ins!pc = MO (Putfield F D); \
3.102 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.103 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.104 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.105 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.106 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.107 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.108 by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.109 by (Clarify_tac 1);
3.110 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
3.111 @@ -231,8 +231,8 @@
3.112 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.113 \ ins!pc = MO mo_com; \
3.114 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.115 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.116 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.117 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.118 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.119 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.120 ba 1;
3.121 ba 1;
3.122 @@ -250,12 +250,12 @@
3.123
3.124 Goal
3.125 "\\<lbrakk> wf_prog wt G; \
3.126 -\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
3.127 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.128 \ ins!pc = CO(New cl_idx); \
3.129 -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
3.130 -\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
3.131 -\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
3.132 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.133 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.134 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.135 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.136 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.137 by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
3.138 approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
3.139 approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
3.140 @@ -271,8 +271,8 @@
3.141 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.142 \ ins!pc = CO co_com; \
3.143 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.144 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.145 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.146 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.147 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.148 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.149 ba 1;
3.150 ba 1;
3.151 @@ -287,11 +287,11 @@
3.152 Goal
3.153 "\\<lbrakk> wt_jvm_prog G phi; \
3.154 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.155 -\ ins ! pc = MI(Invokevirtual mn pTs); \
3.156 +\ ins ! pc = MI(Invoke mn pTs); \
3.157 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.158 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.159 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.160 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.161 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.162 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.163 by(forward_tac [wt_jvm_progD] 1);
3.164 by(etac exE 1);
3.165 by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1
3.166 @@ -361,20 +361,20 @@
3.167 by (fast_tac (claset()
3.168 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
3.169 addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1);
3.170 -qed "Invokevirtual_correct";
3.171 +qed "Invoke_correct";
3.172
3.173 Goal
3.174 "\\<lbrakk> wt_jvm_prog G phi; \
3.175 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.176 \ ins!pc = MI mi_com; \
3.177 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.178 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.179 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.180 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.181 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.182 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.183 ba 1;
3.184 ba 1;
3.185 by (exhaust_tac "mi_com" 1);
3.186 -by (ALLGOALS (fast_tac (claset() addIs [Invokevirtual_correct])));
3.187 +by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
3.188 qed "MI_correct";
3.189
3.190 (****** MR ******)
3.191 @@ -395,11 +395,11 @@
3.192 Goal
3.193 "\\<lbrakk> wt_jvm_prog G phi; \
3.194 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.195 -\ ins ! pc = MR; \
3.196 +\ ins ! pc = MR Return; \
3.197 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.198 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.199 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.200 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.201 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.202 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.203 by (asm_full_simp_tac (simpset() addsimps defs1) 1);
3.204 by (Clarify_tac 1);
3.205 by (asm_full_simp_tac (simpset() addsimps defs1) 1);
3.206 @@ -424,13 +424,14 @@
3.207 Goal
3.208 "\\<lbrakk> wt_jvm_prog G phi; \
3.209 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.210 -\ ins!pc = MR; \
3.211 +\ ins!pc = MR mr; \
3.212 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.213 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.214 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.215 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.216 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.217 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.218 ba 1;
3.219 ba 1;
3.220 +by (exhaust_tac "mr" 1);
3.221 by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
3.222 qed "MR_correct";
3.223
3.224 @@ -441,8 +442,8 @@
3.225 \ ins ! pc = BR(Goto branch); \
3.226 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.227 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.228 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.229 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.230 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.231 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.232 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
3.233 addss (simpset() addsimps defs1)) 1);
3.234 qed "Goto_correct";
3.235 @@ -454,8 +455,8 @@
3.236 \ ins!pc = BR(Ifcmpeq branch); \
3.237 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.238 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.239 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.240 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.241 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.242 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.243 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.244 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
3.245 qed "Ifiacmpeq_correct";
3.246 @@ -466,8 +467,8 @@
3.247 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.248 \ ins!pc = BR br_com; \
3.249 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.250 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.251 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.252 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.253 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.254 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.255 ba 1;
3.256 ba 1;
3.257 @@ -485,8 +486,8 @@
3.258 \ ins ! pc = OS Pop; \
3.259 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.260 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.261 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.262 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.263 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.264 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.265 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.266 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
3.267 qed "Pop_correct";
3.268 @@ -498,8 +499,8 @@
3.269 \ ins ! pc = OS Dup; \
3.270 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.271 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.272 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.273 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.274 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.275 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.276 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.277 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
3.278 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.279 @@ -512,8 +513,8 @@
3.280 \ ins ! pc = OS Dup_x1; \
3.281 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.282 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.283 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.284 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.285 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.286 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.287 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.288 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
3.289 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.290 @@ -525,8 +526,8 @@
3.291 \ ins ! pc = OS Dup_x2; \
3.292 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.293 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.294 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.295 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.296 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.297 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.298 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.299 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
3.300 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.301 @@ -538,8 +539,8 @@
3.302 \ ins ! pc = OS Swap; \
3.303 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.304 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.305 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.306 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.307 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.308 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.309 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.310 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
3.311 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.312 @@ -550,8 +551,8 @@
3.313 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.314 \ ins!pc = OS os_com; \
3.315 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.316 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.317 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.318 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.319 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.320 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.321 ba 1;
3.322 ba 1;
3.323 @@ -563,15 +564,15 @@
3.324 (** Main **)
3.325
3.326 Goalw [correct_state_def,Let_def]
3.327 - "correct_state G phi (None,hp,(stk,loc,C,sig,pc)#fs) \
3.328 -\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) sig = Some(C,meth)";
3.329 + "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \
3.330 +\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) ml = Some(C,meth)";
3.331 by(Asm_full_simp_tac 1);
3.332 by(Blast_tac 1);
3.333 qed "correct_state_impl_Some_cmethd";
3.334
3.335 Goal
3.336 -"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; correct_state G phi state\\<rbrakk> \
3.337 -\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> correct_state G phi state'";
3.338 +"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \
3.339 +\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
3.340 by(split_all_tac 1);
3.341 by(rename_tac "xp hp frs" 1);
3.342 by (exhaust_tac "xp" 1);
3.343 @@ -596,9 +597,8 @@
3.344 qed_spec_mp "exec_lemma";
3.345
3.346 Goal
3.347 -"\\<lbrakk> wt_jvm_prog G phi; \
3.348 -\ correct_state G phi (xp,hp,frs); xp=None; frs\\<noteq>[] \\<rbrakk> \
3.349 -\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs') \\<and> correct_state G phi (xp',hp',frs')";
3.350 +"\\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[] \\<rbrakk> \
3.351 +\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec(G,xp,hp,frs) = Some(xp',hp',frs') \\<and> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.352 by (dres_inst_tac [("G","G"),("hp","hp")] exec_lemma 1);
3.353 ba 1;
3.354 by (fast_tac (claset() addIs [BV_correct_1]) 1);
3.355 @@ -606,8 +606,7 @@
3.356 (*******)
3.357
3.358 Goalw [exec_all_def]
3.359 -"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \
3.360 -\ \\<Longrightarrow> correct_state G phi s \\<longrightarrow> correct_state G phi t";
3.361 +"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \\<Longrightarrow> G,phi \\<turnstile>JVM s\\<surd> \\<longrightarrow> G,phi \\<turnstile>JVM t\\<surd>";
3.362 be rtrancl_induct 1;
3.363 by (Simp_tac 1);
3.364 by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1);
3.365 @@ -615,7 +614,7 @@
3.366
3.367
3.368 Goal
3.369 -"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,cn,ml,pc)#frs); correct_state G phi s0 \\<rbrakk> \
3.370 +"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,cn,ml,pc)#frs); G,phi \\<turnstile>JVM s0 \\<surd>\\<rbrakk> \
3.371 \ \\<Longrightarrow> approx_stk G hp stk (fst (((phi cn) ml) ! pc)) \\<and> approx_loc G hp loc (snd (((phi cn) ml) ! pc)) ";
3.372 bd BV_correct 1;
3.373 ba 1;
4.1 --- a/src/HOL/MicroJava/BV/Correct.ML Wed Nov 24 13:36:14 1999 +0100
4.2 +++ b/src/HOL/MicroJava/BV/Correct.ML Thu Nov 25 12:01:28 1999 +0100
4.3 @@ -233,7 +233,7 @@
4.4 (** hconf **)
4.5
4.6
4.7 -Goal "hp x = None \\<longrightarrow> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp(newref hp\\<mapsto>obj)\\<turnstile>\\<surd>";
4.8 +Goal "hp x = None \\<longrightarrow> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G\\<turnstile>h hp(newref hp\\<mapsto>obj)\\<surd>";
4.9 by (asm_full_simp_tac (simpset() addsplits [split_split]
4.10 addsimps [hconf_def]) 1);
4.11 by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1);
4.12 @@ -241,7 +241,7 @@
4.13
4.14
4.15 Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \
4.16 -\ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<turnstile>\\<surd>";
4.17 +\ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G\\<turnstile>h hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<surd>";
4.18 by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1);
4.19 by (fast_tac (claset() addIs
4.20 [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update]
5.1 --- a/src/HOL/MicroJava/BV/Correct.thy Wed Nov 24 13:36:14 1999 +0100
5.2 +++ b/src/HOL/MicroJava/BV/Correct.thy Thu Nov 25 12:01:28 1999 +0100
5.3 @@ -35,7 +35,7 @@
5.4 in
5.5 (\\<exists>rT maxl ins.
5.6 cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
5.7 - (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invokevirtual mn pTs) \\<and>
5.8 + (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invoke mn pTs) \\<and>
5.9 (mn,pTs) = ml0 \\<and>
5.10 (\\<exists>apTs D ST'.
5.11 fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\<and>
5.12 @@ -49,6 +49,7 @@
5.13
5.14 constdefs
5.15 correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool"
5.16 + ("_,_\\<turnstile>JVM _\\<surd>" [51,51] 50)
5.17 "correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs).
5.18 case xp of
5.19 None \\<Rightarrow> (case frs of
5.20 @@ -57,7 +58,7 @@
5.21 in
5.22 \\<exists>rT maxl ins.
5.23 cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
5.24 - G,hp\\<turnstile>\\<surd> \\<and>
5.25 + G\\<turnstile>h hp\\<surd> \\<and>
5.26 correct_frame G hp ((phi C ml) ! pc) maxl ins f \\<and>
5.27 correct_frames G hp phi rT C ml fs))
5.28 | Some x \\<Rightarrow> True"
6.1 --- a/src/HOL/MicroJava/J/Conform.ML Wed Nov 24 13:36:14 1999 +0100
6.2 +++ b/src/HOL/MicroJava/J/Conform.ML Thu Nov 25 12:01:28 1999 +0100
6.3 @@ -210,11 +210,11 @@
6.4
6.5 section "hconf";
6.6
6.7 -Goalw [hconf_def] "\\<lbrakk>G,h\\<turnstile>\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
6.8 +Goalw [hconf_def] "\\<lbrakk>G\\<turnstile>h h\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
6.9 by (Fast_tac 1);
6.10 qed "hconfD";
6.11
6.12 -Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G,h\\<turnstile>\\<surd>";
6.13 +Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G\\<turnstile>h h\\<surd>";
6.14 by (Fast_tac 1);
6.15 qed "hconfI";
6.16
6.17 @@ -222,7 +222,7 @@
6.18 section "conforms";
6.19
6.20 val conforms_heapD = prove_goalw thy [conforms_def]
6.21 - "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>\\<surd>"
6.22 + "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G\\<turnstile>h h\\<surd>"
6.23 (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
6.24
6.25 val conforms_localD = prove_goalw thy [conforms_def]
6.26 @@ -230,12 +230,12 @@
6.27 cut_facts_tac prems 1, Asm_full_simp_tac 1]);
6.28
6.29 val conformsI = prove_goalw thy [conforms_def]
6.30 -"\\<lbrakk>G,h\\<turnstile>\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
6.31 +"\\<lbrakk>G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
6.32 cut_facts_tac prems 1,
6.33 Simp_tac 1,
6.34 Auto_tac]);
6.35
6.36 -Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G,h'\\<turnstile>\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
6.37 +Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
6.38 by( fast_tac (HOL_cs addDs [conforms_localD]
6.39 addSEs [conformsI, lconf_hext]) 1);
6.40 qed "conforms_hext";
7.1 --- a/src/HOL/MicroJava/J/Conform.thy Wed Nov 24 13:36:14 1999 +0100
7.2 +++ b/src/HOL/MicroJava/J/Conform.thy Thu Nov 25 12:01:28 1999 +0100
7.3 @@ -23,10 +23,10 @@
7.4 oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50)
7.5 "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))"
7.6
7.7 - hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_,_\\<turnstile>\\<surd>" [51,51] 50)
7.8 - "G,h\\<turnstile>\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
7.9 + hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50)
7.10 + "G\\<turnstile>h h\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
7.11
7.12 conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
7.13 - "s\\<Colon>\\<preceq>E \\<equiv> prg E,heap s\\<turnstile>\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
7.14 + "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
7.15
7.16 end
8.1 --- a/src/HOL/MicroJava/J/Type.thy Wed Nov 24 13:36:14 1999 +0100
8.2 +++ b/src/HOL/MicroJava/J/Type.thy Thu Nov 25 12:01:28 1999 +0100
8.3 @@ -25,7 +25,7 @@
8.4 datatype ref_ty (* reference type, cf. 4.3 *)
8.5 = NullT (* null type, cf. 4.1 *)
8.6 | ClassT cname (* class type *)
8.7 -and ty (* any type, cf. 4.1 *)
8.8 +datatype ty (* any type, cf. 4.1 *)
8.9 = PrimT prim_ty (* primitive type *)
8.10 | RefT ref_ty (* reference type *)
8.11
9.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Nov 24 13:36:14 1999 +0100
9.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Thu Nov 25 12:01:28 1999 +0100
9.3 @@ -14,7 +14,7 @@
9.4 | MO manipulate_object
9.5 | CH check_object
9.6 | MI meth_inv
9.7 - | MR
9.8 + | MR meth_ret
9.9 | OS op_stack
9.10 | BR branch
9.11
9.12 @@ -51,7 +51,7 @@
9.13 in
9.14 (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
9.15
9.16 - | MR \\<Rightarrow> (let frs' = exec_mr stk frs in
9.17 + | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
9.18 (None,hp,frs'))
9.19
9.20 | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
10.1 --- a/src/HOL/MicroJava/JVM/Method.ML Wed Nov 24 13:36:14 1999 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,7 +0,0 @@
10.4 -(* Title: HOL/MicroJava/JVM/Method.ML
10.5 - ID: $Id$
10.6 - Author: Cornelia Pusch
10.7 - Copyright 1999 Technische Universitaet Muenchen
10.8 -*)
10.9 -
10.10 -Addsimps [exec_mr_def];
11.1 --- a/src/HOL/MicroJava/JVM/Method.thy Wed Nov 24 13:36:14 1999 +0100
11.2 +++ b/src/HOL/MicroJava/JVM/Method.thy Thu Nov 25 12:01:28 1999 +0100
11.3 @@ -12,13 +12,13 @@
11.4
11.5 datatype
11.6 meth_inv =
11.7 - Invokevirtual mname (ty list) (** inv. instance meth of an object **)
11.8 + Invoke mname (ty list) (** inv. instance meth of an object **)
11.9
11.10 consts
11.11 exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count]
11.12 \\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)"
11.13 primrec
11.14 - "exec_mi (Invokevirtual mn ps) G hp stk pc =
11.15 + "exec_mi (Invoke mn ps) G hp stk pc =
11.16 (let n = length ps;
11.17 argsoref = take (n+1) stk;
11.18 oref = last argsoref;
11.19 @@ -30,11 +30,14 @@
11.20 (xp' , frs' , drop (n+1) stk , pc+1))"
11.21
11.22
11.23 -constdefs
11.24 - exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
11.25 -"exec_mr stk0 frs \\<equiv>
11.26 - (let val = hd stk0;
11.27 - (stk,loc,cn,met,pc) = hd frs
11.28 +datatype
11.29 + meth_ret = Return
11.30 +
11.31 +consts
11.32 + exec_mr :: "[meth_ret,opstack,frame list] \\<Rightarrow> frame list"
11.33 +primrec
11.34 + "exec_mr Return stk0 frs =
11.35 + (let val = hd stk0; (stk,loc,cn,met,pc) = hd frs
11.36 in
11.37 (val#stk,loc,cn,met,pc)#tl frs)"
11.38