1 (* Title: HOL/MicroJava/JVM/JVMState.thy |
1 (* Title: HOL/MicroJava/JVM/JVMState.thy |
2 Author: Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen |
2 Author: Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen |
3 *) |
3 *) |
4 |
4 |
5 chapter {* Java Virtual Machine \label{cha:jvm} *} |
5 chapter \<open>Java Virtual Machine \label{cha:jvm}\<close> |
6 |
6 |
7 section {* State of the JVM *} |
7 section \<open>State of the JVM\<close> |
8 |
8 |
9 theory JVMState |
9 theory JVMState |
10 imports "../J/Conform" |
10 imports "../J/Conform" |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Frame Stack *} |
13 subsection \<open>Frame Stack\<close> |
14 type_synonym opstack = "val list" |
14 type_synonym opstack = "val list" |
15 type_synonym locvars = "val list" |
15 type_synonym locvars = "val list" |
16 type_synonym p_count = nat |
16 type_synonym p_count = nat |
17 |
17 |
18 type_synonym |
18 type_synonym |
27 -- "name of class where current method is defined" |
27 -- "name of class where current method is defined" |
28 -- "method name + parameter types" |
28 -- "method name + parameter types" |
29 -- "program counter within frame" |
29 -- "program counter within frame" |
30 |
30 |
31 |
31 |
32 subsection {* Exceptions *} |
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 {* Runtime State *} |
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" -- "exception flag, heap, frames" |
39 |
39 |
40 |
40 |
41 subsection {* Lemmas *} |
41 subsection \<open>Lemmas\<close> |
42 |
42 |
43 lemma new_Addr_OutOfMemory: |
43 lemma new_Addr_OutOfMemory: |
44 "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
44 "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
45 proof - |
45 proof - |
46 obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |
46 obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |