Quelle  JVMExec.thy

(*  Title:      HOL/MicroJava/JVM/JVMExec.thy
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Program Execution in the JVM›

theory JVMExec
imports JVMExecInstr JVMExceptions
begin

abbreviation
  instrs_of :: "jvm_prog ==> cname ==> mname ==> instr list" where
  "instrs_of P C M == fst(snd(snd(snd(snd(snd(method P C M))))))"

fun exec :: "jvm_prog × jvm_state => jvm_state option" where ― ‹single step execution›
  "exec (P, xp, h, []) = None"

| "exec (P, None, h, (stk,loc,C,M,pc)#frs) =
  (let
     i = instrs_of P C M ! pc;
     (xcpt', h', frs') = exec_instr i P h stk loc C M pc frs
   in Some(case xcpt' of
             None ==> (None,h',frs')
           | Some a ==> find_handler P a h ((stk,loc,C,M,pc)#frs)))"

| "exec (P, Some xa, h, frs) = None" 

― ‹relational view›
inductive_set
  exec_1 :: "jvm_prog ==> (jvm_state × jvm_state) set"
  and exec_1' :: "jvm_prog ==> jvm_state ==> jvm_state ==> bool" 
    (‹_ ⊨/ _ -jvm→₁/ _› [61,61,61] 60)
  for P :: jvm_prog
where
  "P ⊨ σ -jvm→₁ σ' ≡ (σ,σ') ∈ exec_1 P"
| exec_1I: "exec (P,σ) = Some σ' ==> P ⊨ σ -jvm→₁ σ'"

― ‹reflexive transitive closure:›
definition exec_all :: "jvm_prog ==> jvm_state ==> jvm_state ==> bool"
    (‹(_ ⊨/ _ -jvm→/ _)› [61,61,61]60) where
(* FIXME exec_all \<rightarrow> exec_star, also in Def.JVM *)
  exec_all_def1: "P ⊨ σ -jvm→ σ' ⟷ (σ,σ') ∈ (exec_1 P)^*"

notation (ASCII)
  exec_all  (‹_ |-/ _ -jvm->/ _› [61,61,61]60)


lemma exec_1_eq:
  "exec_1 P = {(σ,σ'). exec (P,σ) = Some σ'}"
(*<*)by (auto intro: exec_1I elim: exec_1.cases)(*>*)

lemma exec_1_iff:
  "P ⊨ σ -jvm→₁ σ' = (exec (P,σ) = Some σ')"
(*<*)by (simp add: exec_1_eq)(*>*)

lemma exec_all_def:
  "P ⊨ σ -jvm→ σ' = ((σ,σ') ∈ {(σ,σ'). exec (P,σ) = Some σ'}^*)"
(*<*)by (simp add: exec_all_def1 exec_1_eq)(*>*)

lemma jvm_refl[iff]: "P ⊨ σ -jvm→ σ"
(*<*)by(simp add: exec_all_def)(*>*)

lemma jvm_trans[trans]:
 "[ P ⊨ σ -jvm→ σ'; P ⊨ σ' -jvm→ σ'' ] ==> P ⊨ σ -jvm→ σ''"
(*<*)by(simp add: exec_all_def)(*>*)

lemma jvm_one_step1[trans]:
 "[ P ⊨ σ -jvm→₁ σ'; P ⊨ σ' -jvm→ σ'' ] ==> P ⊨ σ -jvm→ σ''"
(*<*) by (simp add: exec_all_def1) (*>*)

lemma jvm_one_step2[trans]:
 "[ P ⊨ σ -jvm→ σ'; P ⊨ σ' -jvm→₁ σ'' ] ==> P ⊨ σ -jvm→ σ''"
(*<*) by (simp add: exec_all_def1) (*>*)

lemma exec_all_conf:
  "[ P ⊨ σ -jvm→ σ'; P ⊨ σ -jvm→ σ'' ]
  ==> P ⊨ σ' -jvm→ σ'' ∨ P ⊨ σ'' -jvm→ σ'"
(*<*)by(simp add: exec_all_def single_valued_def single_valued_confluent)(*>*)


lemma exec_all_finalD: "P ⊨ (x, h, []) -jvm→ σ ==> σ = (x, h, [])"
(*<*)
proof -
  assume "P ⊨ (x, h, []) -jvm→ σ"
  then have "((x, h, []), σ) ∈ {(σ, σ'). exec (P, σ) = ⌊σ'⌋}^*"
    by(simp only: exec_all_def)
  then show ?thesis proof(rule converse_rtranclE) qed simp+
qed
(*>*)

lemma exec_all_deterministic:
  "[ P ⊨ σ -jvm→ (x,h,[]); P ⊨ σ -jvm→ σ' ] ==> P ⊨ σ' -jvm→ (x,h,[])"
(*<*)
proof -
  assume assms: "P ⊨ σ -jvm→ (x,h,[])" "P ⊨ σ -jvm→ σ'"
  show ?thesis using exec_all_conf[OF assms]
    by(blast dest!: exec_all_finalD)
qed
(*>*)


text ‹
 The start configuration of the JVM: in the start heap, we call a
 method ‹m› of class ‹C› in program ‹P›. The
 ‹this› pointer of the frame is set to ‹Null› to simulate
 a static method invokation.
 ›
definition start_state :: "jvm_prog ==> cname ==> mname ==> jvm_state" where
  "start_state P C M =
  (let (D,Ts,T,mxs,mxl₀,b) = method P C M in
    (None, start_heap P, [([], Null # replicate mxl₀ undefined, C, M, 0)]))"

end