1(*  Title:      HOL/MicroJava/JVM/JVMExec.thy
2    Author:     Cornelia Pusch, Gerwin Klein
3    Copyright   1999 Technische Universitaet Muenchen
4*)
5
6section \<open>Program Execution in the JVM\<close>
7
8theory JVMExec imports JVMExecInstr JVMExceptions begin
9
10
11fun
12  exec :: "jvm_prog \<times> jvm_state => jvm_state option"
13\<comment> \<open>exec is not recursive. fun is just used for pattern matching\<close>
14where
15  "exec (G, xp, hp, []) = None"
16
17| "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
18  (let 
19     i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc;
20     (xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs
21   in Some (find_handler G xcpt' hp' frs'))"
22
23| "exec (G, Some xp, hp, frs) = None" 
24
25
26definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
27              ("_ \<turnstile> _ \<midarrow>jvm\<rightarrow> _" [61,61,61]60) where
28  "G \<turnstile> s \<midarrow>jvm\<rightarrow> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}\<^sup>*"
29
30
31text \<open>
32  The start configuration of the JVM: in the start heap, we call a 
33  method \<open>m\<close> of class \<open>C\<close> in program \<open>G\<close>. The 
34  \<open>this\<close> pointer of the frame is set to \<open>Null\<close> to simulate
35  a static method invokation.
36\<close>
37definition start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" where
38  "start_state G C m \<equiv>
39  let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in
40    (None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])"
41
42end
43