Theory JVMExec

(*  Title:      HOL/MicroJava/JVM/JVMExec.thy
    ID:         $Id: JVMExec.thy,v 1.9.2.7 2002/03/09 22:12:50 kleing Exp $
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Program Execution in the JVM} *}

theory JVMExec
imports JVMExecInstr JVMExceptions
begin

consts
  exec :: "jvm_prog × jvm_state => jvm_state option"


-- "recdef only used for pattern matching"
recdef exec "{}"
  "exec (G, xp, shp, hp, ihp, []) = None"

  "exec (G, None, shp, hp, ihp, (stk,loc,C,sig,pc,z)#frs) =
  (let 
     i = fst(snd(snd(snd(snd(the(method' (G,C) sig)))))) ! pc;
     (xcpt', shp', hp', ihp', frs') = exec_instr i G shp hp ihp stk loc C sig pc z frs
   in Some (find_handler G xcpt' shp' hp' ihp' frs'))"

  "exec (G, Some xp, hp, ihp, frs) = None" 


constdefs
  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
              ("_ |- _ -jvm-> _" [61,61,61]60)
  "G |- s -jvm-> t == (s,t) ∈ {(s,t). exec(G,s) = Some t}^*"


syntax (xsymbols)
  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)

text {*
  The start configuration of the JVM: in the start heap, we call a 
  method @{text m} of class @{text C} in program @{text G}. The 
  @{text this} pointer of the frame is set to @{text Null} to simulate
  a static method invokation.
*}
constdefs  
  start_state :: "jvm_prog => cname => mname => jvm_state"
  "start_state G C m ≡
  let (C',rT,mxs,mxl,ins,et) = the (method (G,C) (m,[])) in
  (None,start_sheap G, start_heap G, start_iheap, 
   [([], Null # replicate mxl arbitrary, C, (m,[]), 0, (Null,Null))])"

end