equal
deleted
inserted
replaced
7 |
7 |
8 theory LBVJVM |
8 theory LBVJVM |
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 type_synonym prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list" |
13 |
13 |
14 definition check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where |
14 definition check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where |
15 "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> |
16 (\<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" |
17 |
17 |