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