10 theory BVSpec = Step: |
10 theory BVSpec = Step: |
11 |
11 |
12 constdefs |
12 constdefs |
13 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool" |
13 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool" |
14 "wt_instr i G rT phi mxs max_pc pc == |
14 "wt_instr i G rT phi mxs max_pc pc == |
15 app i G mxs rT (phi!pc) \\<and> |
15 app i G mxs rT (phi!pc) \<and> |
16 (\\<forall> pc' \\<in> set (succs i pc). pc' < max_pc \\<and> (G \\<turnstile> step i G (phi!pc) <=' phi!pc'))" |
16 (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))" |
17 |
17 |
18 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" |
18 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" |
19 "wt_start G C pTs mxl phi == |
19 "wt_start G C pTs mxl phi == |
20 G \\<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" |
20 G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" |
21 |
21 |
22 |
22 |
23 wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool" |
23 wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool" |
24 "wt_method G C pTs rT mxs mxl ins phi == |
24 "wt_method G C pTs rT mxs mxl ins phi == |
25 let max_pc = length ins |
25 let max_pc = length ins |
26 in |
26 in |
27 0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and> |
27 0 < max_pc \<and> wt_start G C pTs mxl phi \<and> |
28 (\\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)" |
28 (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)" |
29 |
29 |
30 wt_jvm_prog :: "[jvm_prog,prog_type] => bool" |
30 wt_jvm_prog :: "[jvm_prog,prog_type] => bool" |
31 "wt_jvm_prog G phi == |
31 "wt_jvm_prog G phi == |
32 wf_prog (\\<lambda>G C (sig,rT,(maxs,maxl,b)). |
32 wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)). |
33 wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G" |
33 wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G" |
34 |
34 |
35 |
35 |
36 |
36 |
37 lemma wt_jvm_progD: |
37 lemma wt_jvm_progD: |
38 "wt_jvm_prog G phi ==> (\\<exists>wt. wf_prog wt G)" |
38 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)" |
39 by (unfold wt_jvm_prog_def, blast) |
39 by (unfold wt_jvm_prog_def, blast) |
40 |
40 |
41 lemma wt_jvm_prog_impl_wt_instr: |
41 lemma wt_jvm_prog_impl_wt_instr: |
42 "[| wt_jvm_prog G phi; is_class G C; |
42 "[| wt_jvm_prog G phi; is_class G C; |
43 method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] |
43 method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] |
46 simp, simp, simp add: wf_mdecl_def wt_method_def) |
46 simp, simp, simp add: wf_mdecl_def wt_method_def) |
47 |
47 |
48 lemma wt_jvm_prog_impl_wt_start: |
48 lemma wt_jvm_prog_impl_wt_start: |
49 "[| wt_jvm_prog G phi; is_class G C; |
49 "[| wt_jvm_prog G phi; is_class G C; |
50 method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> |
50 method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> |
51 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)" |
51 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)" |
52 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
52 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
53 simp, simp, simp add: wf_mdecl_def wt_method_def) |
53 simp, simp, simp add: wf_mdecl_def wt_method_def) |
54 |
54 |
55 text {* for most instructions wt\_instr collapses: *} |
55 text {* for most instructions wt\_instr collapses: *} |
56 lemma |
56 lemma |
57 "succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = |
57 "succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = |
58 (app i G mxs rT (phi!pc) \\<and> pc+1 < max_pc \\<and> (G \\<turnstile> step i G (phi!pc) <=' phi!(pc+1)))" |
58 (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))" |
59 by (simp add: wt_instr_def) |
59 by (simp add: wt_instr_def) |
60 |
60 |
61 |
61 |
62 (* ### move to WellForm *) |
|
63 |
|
64 lemma methd: |
|
65 "[| wf_prog wf_mb G; (C,S,fs,mdecls) \\<in> set G; (sig,rT,code) \\<in> set mdecls |] |
|
66 ==> method (G,C) sig = Some(C,rT,code) \\<and> is_class G C" |
|
67 proof - |
|
68 assume wf: "wf_prog wf_mb G" |
|
69 assume C: "(C,S,fs,mdecls) \\<in> set G" |
|
70 |
|
71 assume m: "(sig,rT,code) \\<in> set mdecls" |
|
72 moreover |
|
73 from wf |
|
74 have "class G Object = Some (arbitrary, [], [])" |
|
75 by simp |
|
76 moreover |
|
77 from wf C |
|
78 have c: "class G C = Some (S,fs,mdecls)" |
|
79 by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI) |
|
80 ultimately |
|
81 have O: "C \\<noteq> Object" |
|
82 by auto |
|
83 |
|
84 from wf C |
|
85 have "unique mdecls" |
|
86 by (unfold wf_prog_def wf_cdecl_def) auto |
|
87 |
|
88 hence "unique (map (\\<lambda>(s,m). (s,C,m)) mdecls)" |
|
89 by - (induct mdecls, auto) |
|
90 |
|
91 with m |
|
92 have "map_of (map (\\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)" |
|
93 by (force intro: map_of_SomeI) |
|
94 |
|
95 with wf C m c O |
|
96 show ?thesis |
|
97 by (auto simp add: is_class_def dest: method_rec [of _ _ C]) |
|
98 qed |
|
99 |
62 |
100 |
63 |
101 end |
64 end |
102 |
65 |
103 |
66 |