--- a/src/HOL/MicroJava/JVM/JVMState.thy Sun Dec 16 00:18:44 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Sun Dec 16 00:19:08 2001 +0100
@@ -1,43 +1,70 @@
(* Title: HOL/MicroJava/JVM/JVMState.thy
ID: $Id$
- Author: Cornelia Pusch
+ Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
-
header {* State of the JVM *}
-
theory JVMState = Conform:
-
-text {* frame stack :*}
+section {* Frame Stack *}
types
- opstack = "val list"
- locvars = "val list"
- p_count = nat
+ opstack = "val list"
+ locvars = "val list"
+ p_count = nat
- frame = "opstack \<times>
- locvars \<times>
- cname \<times>
- sig \<times>
+ frame = "opstack \<times>
+ locvars \<times>
+ cname \<times>
+ sig \<times>
p_count"
- (* operand stack *)
- (* local variables *)
- (* name of def. class defined *)
- (* meth name+param_desc *)
- (* program counter within frame *)
+ -- "operand stack"
+ -- "local variables (including this pointer and method parameters)"
+ -- "name of class where current method is defined"
+ -- "method name + parameter types"
+ -- "program counter within frame"
+
+
+section {* Exceptions *}
+constdefs
+ raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option"
+ "raise_system_xcpt b x == if b then Some (Addr (XcptRef x)) else None"
+
+ -- "redefines State.new\\_Addr:"
+ new_Addr :: "aheap => loc \<times> val option"
+ "new_Addr h == SOME (a,x). (h a = None \<and> x = None) |
+ x = raise_system_xcpt True OutOfMemory"
+
+
+section {* Runtime State *}
+types
+ jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames"
-text {* exceptions: *}
-constdefs
- raise_xcpt :: "bool => xcpt => xcpt option"
- "raise_xcpt c x == (if c then Some x else None)"
-
+section {* Lemmas *}
-text {* runtime state: *}
-types
- jvm_state = "xcpt option \<times> aheap \<times> frame list"
+lemma new_AddrD:
+ "new_Addr hp = (ref, xcp) \<Longrightarrow> hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
+ apply (drule sym)
+ apply (unfold new_Addr_def)
+ apply (simp add: raise_system_xcpt_def)
+ apply (simp add: Pair_fst_snd_eq Eps_split)
+ apply (rule someI)
+ apply (rule disjI2)
+ apply (rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
+ apply auto
+ done
-end
+lemma new_Addr_OutOfMemory:
+ "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
+proof -
+ obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
+ moreover
+ assume "snd (new_Addr hp) = Some xcp"
+ ultimately
+ show ?thesis by (auto dest: new_AddrD)
+qed
+
+end
\ No newline at end of file