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