equal
deleted
inserted
replaced
20 locvars \<times> |
20 locvars \<times> |
21 cname \<times> |
21 cname \<times> |
22 sig \<times> |
22 sig \<times> |
23 p_count" |
23 p_count" |
24 |
24 |
25 -- "operand stack" |
25 \<comment> "operand stack" |
26 -- "local variables (including this pointer and method parameters)" |
26 \<comment> "local variables (including this pointer and method parameters)" |
27 -- "name of class where current method is defined" |
27 \<comment> "name of class where current method is defined" |
28 -- "method name + parameter types" |
28 \<comment> "method name + parameter types" |
29 -- "program counter within frame" |
29 \<comment> "program counter within frame" |
30 |
30 |
31 |
31 |
32 subsection \<open>Exceptions\<close> |
32 subsection \<open>Exceptions\<close> |
33 definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where |
33 definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where |
34 "raise_system_xcpt b x \<equiv> raise_if b x None" |
34 "raise_system_xcpt b x \<equiv> raise_if b x None" |
35 |
35 |
36 subsection \<open>Runtime State\<close> |
36 subsection \<open>Runtime State\<close> |
37 type_synonym |
37 type_synonym |
38 jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
38 jvm_state = "val option \<times> aheap \<times> frame list" \<comment> "exception flag, heap, frames" |
39 |
39 |
40 |
40 |
41 subsection \<open>Lemmas\<close> |
41 subsection \<open>Lemmas\<close> |
42 |
42 |
43 lemma new_Addr_OutOfMemory: |
43 lemma new_Addr_OutOfMemory: |