# Theory JVMExec

Up to index of Isabelle/HOL/MicroJava

theory JVMExec
imports JVMExecInstr JVMExceptions
begin

    (*  Title:      HOL/MicroJava/JVM/JVMExec.thy
        ID:         $Id: JVMExec.thy,v 1.16 2005/06/17 14:13:09 haftmann 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"

    -- "exec is not recursive. recdef is just used for pattern matching"
    recdef exec "{}"
      "exec (G, xp, hp, []) = None"

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

      "exec (G, Some xp, hp, 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,i,et) = the (method (G,C) (m,[])) in
        (None, start_heap G, [([], Null # replicate mxl arbitrary, C, (m,[]), 0)])"

    end