Theory JVMState

Up to index of Isabelle/HOL/MicroJava

(*  Title:      HOL/MicroJava/JVM/JVMState.thy
    ID:         $Id: JVMState.thy,v 1.4 2000/09/22 11:12:20 kleing Exp $
    Author:     Cornelia Pusch
    Copyright   1999 Technische Universitaet Muenchen
*)


header {* State of the JVM *}


theory JVMState = Store:


text {* frame stack :*}
types
 opstack         = "val list"
 locvars         = "val list" 
 p_count         = nat

 frame = "opstack ×                      
          locvars ×              
          cname ×                        
          sig ×                  
          p_count"

        (* operand stack *)
        (* local variables *)
        (* name of def. class defined *)
        (* meth name+param_desc *)
        (* program counter within frame *)


text {* exceptions: *}
constdefs
  raise_xcpt :: "bool => xcpt => xcpt option"
  "raise_xcpt c x == (if c then Some x else None)"


text {* runtime state: *}
types
  jvm_state = "xcpt option × aheap × frame list"  


text {* dynamic method lookup: *}
constdefs
  dyn_class     :: "'code prog × sig × cname => cname"
  "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))"

end