|
13672
|
1 |
|
|
|
2 |
theory Altern = BVSpec:
|
|
|
3 |
|
|
|
4 |
|
|
|
5 |
constdefs
|
|
|
6 |
check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"
|
|
|
7 |
"check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
|
|
|
8 |
|
|
|
9 |
wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
|
|
|
10 |
exception_table,p_count] \<Rightarrow> bool"
|
|
|
11 |
"wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv>
|
|
|
12 |
app i G mxs rT pc et (phi!pc) \<and>
|
|
|
13 |
check_type G mxs mxr (OK (phi!pc)) \<and>
|
|
|
14 |
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
|
|
|
15 |
|
|
|
16 |
wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
|
|
|
17 |
exception_table,method_type] \<Rightarrow> bool"
|
|
|
18 |
"wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv>
|
|
|
19 |
let max_pc = length ins in
|
|
|
20 |
0 < max_pc \<and>
|
|
|
21 |
length phi = length ins \<and>
|
|
|
22 |
check_bounded ins et \<and>
|
|
|
23 |
wt_start G C pTs mxl phi \<and>
|
|
|
24 |
(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)"
|
|
|
25 |
|
|
|
26 |
|
|
|
27 |
lemma wt_method_wt_method_altern :
|
|
|
28 |
"wt_method G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method_altern G C pTs rT mxs mxl ins et phi"
|
|
|
29 |
apply (simp add: wt_method_def wt_method_altern_def)
|
|
|
30 |
apply (intro strip)
|
|
|
31 |
apply clarify
|
|
|
32 |
apply (drule spec, drule mp, assumption)
|
|
|
33 |
apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def)
|
|
|
34 |
apply (auto intro: imageI)
|
|
|
35 |
done
|
|
|
36 |
|
|
|
37 |
|
|
|
38 |
lemma check_type_check_types [rule_format]:
|
|
|
39 |
"(\<forall>pc. pc < length phi \<longrightarrow> check_type G mxs mxr (OK (phi ! pc)))
|
|
|
40 |
\<longrightarrow> check_types G mxs mxr (map OK phi)"
|
|
|
41 |
apply (induct phi)
|
|
|
42 |
apply (simp add: check_types_def)
|
|
|
43 |
apply (simp add: check_types_def)
|
|
|
44 |
apply clarify
|
|
|
45 |
apply (frule_tac x=0 in spec)
|
|
|
46 |
apply (simp add: check_type_def)
|
|
|
47 |
apply auto
|
|
|
48 |
done
|
|
|
49 |
|
|
|
50 |
lemma wt_method_altern_wt_method [rule_format]:
|
|
|
51 |
"wt_method_altern G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method G C pTs rT mxs mxl ins et phi"
|
|
|
52 |
apply (simp add: wt_method_def wt_method_altern_def)
|
|
|
53 |
apply (intro strip)
|
|
|
54 |
apply clarify
|
|
|
55 |
apply (rule conjI)
|
|
|
56 |
(* show check_types *)
|
|
|
57 |
apply (rule check_type_check_types)
|
|
|
58 |
apply (simp add: wt_instr_altern_def)
|
|
|
59 |
|
|
|
60 |
(* show wt_instr *)
|
|
|
61 |
apply (intro strip)
|
|
|
62 |
apply (drule spec, drule mp, assumption)
|
|
|
63 |
apply (simp add: wt_instr_def wt_instr_altern_def)
|
|
|
64 |
done
|
|
|
65 |
|
|
|
66 |
|
|
|
67 |
end
|