src/HOL/MicroJava/JVM/JVMState.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,61 @@
+(*  Title:      HOL/MicroJava/JVM/JVMState.thy
+    ID:         $Id$
+    Author:     Cornelia Pusch
+    Copyright   1999 Technische Universitaet Muenchen
+
+State of the JVM
+*)
+
+JVMState = Store +
+
+
+(** frame stack **)
+
+types
+ opstack 	 = "val list"
+ locvars 	 = "val list" 
+ p_count 	 = nat
+
+ 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 *)
+
+
+(** exceptions **)
+
+constdefs
+ raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
+"raise_xcpt c x \\<equiv> (if c then Some x else None)"
+
+ heap_update :: "[xcpt option,aheap,aheap] \\<Rightarrow> aheap"
+"heap_update xp hp' hp \\<equiv> if xp=None then hp' else hp"
+
+ stk_update :: "[xcpt option,opstack,opstack] \\<Rightarrow> opstack"
+"stk_update xp stk' stk \\<equiv> if xp=None then stk' else stk"
+
+ xcpt_update :: "[xcpt option,'a,'a] \\<Rightarrow> 'a"
+"xcpt_update xp y' y \\<equiv> if xp=None then y' else y"
+
+(** runtime state **)
+
+types
+ jvm_state = "xcpt option \\<times>		
+	      aheap \\<times>				
+	      frame list"	
+
+
+
+(** dynamic method lookup **)
+
+constdefs
+ dyn_class	:: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
+"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(cmethd(G,C) sig))"
+end