1(*  Title:      HOL/MicroJava/JVM/JVMState.thy
2    Author:     Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
3*)
4
5chapter \<open>Java Virtual Machine \label{cha:jvm}\<close>
6
7section \<open>State of the JVM\<close>
8
9theory JVMState
10imports "../J/Conform"
11begin
12
13subsection \<open>Frame Stack\<close>
14type_synonym opstack = "val list"
15type_synonym locvars = "val list"
16type_synonym p_count = nat
17
18type_synonym
19 frame = "opstack \<times>     
20          locvars \<times>   
21          cname \<times>     
22          sig \<times>     
23          p_count"
24
25  \<comment> \<open>operand stack\<close> 
26  \<comment> \<open>local variables (including this pointer and method parameters)\<close>
27  \<comment> \<open>name of class where current method is defined\<close>
28  \<comment> \<open>method name + parameter types\<close>
29  \<comment> \<open>program counter within frame\<close>
30
31
32subsection \<open>Exceptions\<close>
33definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where
34  "raise_system_xcpt b x \<equiv> raise_if b x None"
35
36subsection \<open>Runtime State\<close>
37type_synonym
38  jvm_state = "val option \<times> aheap \<times> frame list"  \<comment> \<open>exception flag, heap, frames\<close>
39
40
41subsection \<open>Lemmas\<close>
42
43lemma new_Addr_OutOfMemory:
44  "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
45proof - 
46  obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
47  moreover
48  assume "snd (new_Addr hp) = Some xcp" 
49  ultimately
50  show ?thesis by (auto dest: new_AddrD)
51qed
52  
53end
54