9 imports Typing_Framework_JVM |
9 imports Typing_Framework_JVM |
10 begin |
10 begin |
11 |
11 |
12 types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list" |
12 types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list" |
13 |
13 |
14 constdefs |
14 definition check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where |
15 check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" |
|
16 "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and> |
15 "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and> |
17 (\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None" |
16 (\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None" |
18 |
17 |
19 lbvjvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> |
18 definition lbvjvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> |
20 JVMType.state list \<Rightarrow> instr list \<Rightarrow> JVMType.state \<Rightarrow> JVMType.state" |
19 JVMType.state list \<Rightarrow> instr list \<Rightarrow> JVMType.state \<Rightarrow> JVMType.state" where |
21 "lbvjvm G maxs maxr rT et cert bs \<equiv> |
20 "lbvjvm G maxs maxr rT et cert bs \<equiv> |
22 wtl_inst_list bs cert (JVMType.sup G maxs maxr) (JVMType.le G maxs maxr) Err (OK None) (exec G maxs rT et bs) 0" |
21 wtl_inst_list bs cert (JVMType.sup G maxs maxr) (JVMType.le G maxs maxr) Err (OK None) (exec G maxs rT et bs) 0" |
23 |
22 |
24 wt_lbv :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> |
23 definition wt_lbv :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> |
25 exception_table \<Rightarrow> JVMType.state list \<Rightarrow> instr list \<Rightarrow> bool" |
24 exception_table \<Rightarrow> JVMType.state list \<Rightarrow> instr list \<Rightarrow> bool" where |
26 "wt_lbv G C pTs rT mxs mxl et cert ins \<equiv> |
25 "wt_lbv G C pTs rT mxs mxl et cert ins \<equiv> |
27 check_bounded ins et \<and> |
26 check_bounded ins et \<and> |
28 check_cert G mxs (1+size pTs+mxl) (length ins) cert \<and> |
27 check_cert G mxs (1+size pTs+mxl) (length ins) cert \<and> |
29 0 < size ins \<and> |
28 0 < size ins \<and> |
30 (let start = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); |
29 (let start = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); |
31 result = lbvjvm G mxs (1+size pTs+mxl) rT et cert ins (OK start) |
30 result = lbvjvm G mxs (1+size pTs+mxl) rT et cert ins (OK start) |
32 in result \<noteq> Err)" |
31 in result \<noteq> Err)" |
33 |
32 |
34 wt_jvm_prog_lbv :: "jvm_prog \<Rightarrow> prog_cert \<Rightarrow> bool" |
33 definition wt_jvm_prog_lbv :: "jvm_prog \<Rightarrow> prog_cert \<Rightarrow> bool" where |
35 "wt_jvm_prog_lbv G cert \<equiv> |
34 "wt_jvm_prog_lbv G cert \<equiv> |
36 wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_lbv G C (snd sig) rT maxs maxl et (cert C sig) b) G" |
35 wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_lbv G C (snd sig) rT maxs maxl et (cert C sig) b) G" |
37 |
36 |
38 mk_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list |
37 definition mk_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list |
39 \<Rightarrow> method_type \<Rightarrow> JVMType.state list" |
38 \<Rightarrow> method_type \<Rightarrow> JVMType.state list" where |
40 "mk_cert G maxs rT et bs phi \<equiv> make_cert (exec G maxs rT et bs) (map OK phi) (OK None)" |
39 "mk_cert G maxs rT et bs phi \<equiv> make_cert (exec G maxs rT et bs) (map OK phi) (OK None)" |
41 |
40 |
42 prg_cert :: "jvm_prog \<Rightarrow> prog_type \<Rightarrow> prog_cert" |
41 definition prg_cert :: "jvm_prog \<Rightarrow> prog_type \<Rightarrow> prog_cert" where |
43 "prg_cert G phi C sig \<equiv> let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in |
42 "prg_cert G phi C sig \<equiv> let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in |
44 mk_cert G maxs rT et ins (phi C sig)" |
43 mk_cert G maxs rT et ins (phi C sig)" |
45 |
44 |
46 |
45 |
47 lemma wt_method_def2: |
46 lemma wt_method_def2: |