src/HOL/MicroJava/JVM/JVMState.thy

Cassini identity is easier to prove using INTEGERS

(*  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)"

(** 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(method(G,C) sig))"
end