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 header {* |
5 chapter {* Java Virtual Machine \label{cha:jvm} *} |
6 \chapter{Java Virtual Machine}\label{cha:jvm} |
6 |
7 \isaheader{State of the JVM} |
7 section {* State of the JVM *} |
8 *} |
|
9 |
8 |
10 theory JVMState |
9 theory JVMState |
11 imports "../J/Conform" |
10 imports "../J/Conform" |
12 begin |
11 begin |
13 |
12 |
14 section {* Frame Stack *} |
13 subsection {* Frame Stack *} |
15 type_synonym opstack = "val list" |
14 type_synonym opstack = "val list" |
16 type_synonym locvars = "val list" |
15 type_synonym locvars = "val list" |
17 type_synonym p_count = nat |
16 type_synonym p_count = nat |
18 |
17 |
19 type_synonym |
18 type_synonym |
28 -- "name of class where current method is defined" |
27 -- "name of class where current method is defined" |
29 -- "method name + parameter types" |
28 -- "method name + parameter types" |
30 -- "program counter within frame" |
29 -- "program counter within frame" |
31 |
30 |
32 |
31 |
33 section {* Exceptions *} |
32 subsection {* Exceptions *} |
34 definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where |
33 definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where |
35 "raise_system_xcpt b x \<equiv> raise_if b x None" |
34 "raise_system_xcpt b x \<equiv> raise_if b x None" |
36 |
35 |
37 section {* Runtime State *} |
36 subsection {* Runtime State *} |
38 type_synonym |
37 type_synonym |
39 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" |
40 |
39 |
41 |
40 |
42 section {* Lemmas *} |
41 subsection {* Lemmas *} |
43 |
42 |
44 lemma new_Addr_OutOfMemory: |
43 lemma new_Addr_OutOfMemory: |
45 "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
44 "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
46 proof - |
45 proof - |
47 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") |