Theory JVMSemantics

(* Title: RTS/JVM_RTS/JVMSemantics.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Instantiating @{term Semantics} with Jinja JVM"

theory JVMSemantics
imports "../Common/Semantics" JinjaDCI.JVMExec
begin

fun JVMsmall :: "jvm_prog ⇒ jvm_state ⇒ jvm_state set" where
"JVMsmall P σ = { σ'. exec (P, σ) = Some σ' }"

lemma JVMsmall_prealloc_pres:
assumes pre: "preallocated (fst(snd σ))"
  and "σ' ∈ JVMsmall P σ"
shows "preallocated (fst(snd σ'))"
using exec_prealloc_pres[OF pre] assms by(cases σ, cases σ', auto)

lemma JVMsmall_det: "JVMsmall P σ = {} ∨ (∃σ'. JVMsmall P σ = {σ'})"
by auto

definition JVMendset :: "jvm_state set" where
"JVMendset ≡ { (xp,h,frs,sh). frs = [] ∨ (∃x. xp = Some x) }"

lemma JVMendset_final: "σ ∈ JVMendset ⟹ ∀P. JVMsmall P σ = {}"
 by(auto simp: JVMendset_def)

lemma start_state_nend:
 "start_state P ∉ JVMendset"
 by(simp add: start_state_def JVMendset_def)

interpretation JVMSemantics: Semantics JVMsmall JVMendset
 by unfold_locales (auto dest: JVMendset_final)

end