Up to index of Isabelle/HOL/objinit
theory JVM = Typing_Framework_JVM + Kildall:(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id: JVM.html,v 1.1 2002/11/28 14:12:09 kleing Exp $
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
theory JVM = Typing_Framework_JVM + Kildall:
constdefs
kiljvm :: "jvm_prog \<Rightarrow> cname \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> exception_table \<Rightarrow>
instr list \<Rightarrow> state list \<Rightarrow> state list"
"kiljvm G C maxs maxr rT ini et bs ==
kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G C maxs rT ini et bs)"
wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> nat
\<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> bool"
"wt_kil G C pTs rT ini mxs mxl et ins ==
check_bounded ins et \<and> 0 < size ins \<and>
(let this = OK (if ini \<and> C \<noteq> Object then PartInit C else Init (Class C));
first = Some (([],this#((map OK (map Init pTs)))@(replicate mxl Err)),
C=Object);
start = OK first#(replicate (size ins - 1) (OK None));
result = kiljvm G C mxs (1+size pTs+mxl) rT ini et ins start
in \<forall>n < size ins. result!n \<noteq> Err)"
wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool"
"wt_jvm_prog_kildall G ==
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
wt_kil G C (snd sig) rT (fst sig=init) maxs maxl et b) G"
theorem (in start_context) is_bcv_kiljvm:
"bounded step (size bs) \<Longrightarrow>
is_bcv r Err step (size bs) A (kiljvm G C mxs mxr rT (mn=init) et bs)"
apply simp
apply (insert wf)
apply (unfold kiljvm_def)
apply (rule is_bcv_kildall)
apply (simp (no_asm) add: sl_triple_conv [symmetric])
apply (rule semilat_JVM_slI, assumption)
apply (simp (no_asm) add: JVM_le_unfold)
apply (blast intro!: ac_order_init wf_converse_subcls1_impl_acc_init
dest: wf_subcls1 wf_acyclic)
apply (simp add: JVM_le_unfold)
apply (erule exec_pres_type)
apply assumption
apply (erule exec_mono, assumption)
done
lemma subset_replicate: "set (replicate n x) \<subseteq> {x}"
by (induct n) auto
lemma in_set_replicate:
"x \<in> set (replicate n y) \<Longrightarrow> x = y"
proof -
assume "x \<in> set (replicate n y)"
also have "set (replicate n y) \<subseteq> {y}" by (rule subset_replicate)
finally have "x \<in> {y}" .
thus ?thesis by simp
qed
lemma list_appendI:
"\<lbrakk>a \<in> list x A; b \<in> list y A\<rbrakk> \<Longrightarrow> a @ b \<in> list (x+y) A"
apply (unfold list_def)
apply (simp (no_asm))
apply blast
done
lemma (in start_context) start_in_A [intro?]:
"0 < size bs \<Longrightarrow> start \<in> list (size bs) A"
apply (insert pTs C)
apply (simp split del: split_if)
apply (unfold JVM_states_unfold)
apply (auto simp add: map_compose split
intro!: listI list_appendI dest!: in_set_replicate)
apply force+
done
theorem (in start_context) wt_kil_correct:
assumes wtk: "wt_kil G C pTs rT (mn=init) mxs mxl et bs"
shows "\<exists>phi. wt_method G C mn pTs rT mxs mxl bs et phi"
proof -
from wtk obtain res where
ck_bound: "check_bounded bs et" and
result: "res = kiljvm G C mxs mxr rT (mn=init) et bs start" and
success: "\<forall>n < size bs. res!n \<noteq> Err" and
instrs: "0 < size bs"
by (unfold wt_kil_def) (simp add: map_compose)
from ck_bound have bounded: "bounded step (size bs)"
by (simp add: exec_def) (intro bounded_lift check_bounded_is_bounded)
hence bcv:
"is_bcv r Err step (size bs) A (kiljvm G C mxs mxr rT (mn=init) et bs)"
by (rule is_bcv_kiljvm)
from instrs have "start \<in> list (size bs) A" ..
with bcv success result have
"\<exists>ts\<in>list (size bs) A. start <=[r] ts \<and> wt_step r Err step ts"
by (unfold is_bcv_def) blast
then obtain phi' where
in_A: "phi' \<in> list (size bs) A" and
s: "start <=[r] phi'" and
w: "wt_step r Err step phi'"
by blast
hence wt_err_step: "wt_err_step (sup_state_opt G) step phi'"
by (simp add: wt_err_step_def JVM_le_Err_conv)
from in_A have l: "size phi' = size bs" by simp
moreover {
from in_A have "check_types G mxs mxr phi'" by (simp add: check_types_def)
also from w
have [symmetric]: "map OK (map ok_val phi') = phi'"
by (auto intro!: map_id simp add: wt_step_def not_Err_eq)
finally have "check_types G mxs mxr (map OK (map ok_val phi'))" .
}
moreover {
from s have "start!0 <=_r phi'!0" by (rule le_listD) simp
moreover
from instrs w l
have "phi'!0 \<noteq> Err" by (unfold wt_step_def) simp
then obtain phi0 where "phi'!0 = OK phi0" by (auto simp add: not_Err_eq)
ultimately
have "wt_start G C mn pTs mxl (map ok_val phi')" using l instrs
by (unfold wt_start_def) (simp add: map_compose lesub_def JVM_le_Err_conv)
}
moreover
from bounded wt_err_step
have "wt_app_eff (sup_state_opt G) app eff (map ok_val phi')"
by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def)
ultimately
have "wt_method G C mn pTs rT mxs mxl bs et (map ok_val phi')"
using instrs ck_bound by (simp add: wt_method_def2)
thus ?thesis by blast
qed
theorem (in start_context) wt_kil_complete:
assumes wtm: "wt_method G C mn pTs rT mxs mxl bs et phi"
shows "wt_kil G C pTs rT (mn=init) mxs mxl et bs"
proof -
from wtm obtain
instrs: "0 < size bs" and
length: "length phi = length bs" and
ck_bound: "check_bounded bs et" and
ck_type: "check_types G mxs mxr (map OK phi)" and
wt_start: "wt_start G C mn pTs mxl phi" and
app_eff: "wt_app_eff (sup_state_opt G) app eff phi"
by (simp add: wt_method_def2)
from ck_bound have bounded: "bounded step (size bs)"
by (simp add: exec_def) (intro bounded_lift check_bounded_is_bounded)
with app_eff
have "wt_err_step (sup_state_opt G) (err_step (size phi) app eff) (map OK phi)"
by - (erule wt_app_eff_imp_wt_err,simp add: exec_def length)
hence wt_err: "wt_err_step (sup_state_opt G) step (map OK phi)"
by (simp add: exec_def length)
from bounded have is_bcv:
"is_bcv r Err step (size bs) A (kiljvm G C mxs mxr rT (mn=init) et bs)"
by (rule is_bcv_kiljvm)
moreover
from instrs have "start \<in> list (size bs) A" ..
moreover
let ?phi = "map OK phi"
have less_phi: "start <=[r] ?phi"
proof (rule le_listI)
from length instrs
show "length start = length (map OK phi)" by simp
next
fix n
from wt_start have "G \<turnstile> ok_val (start!0) <=' phi!0"
by (simp add: wt_start_def map_compose)
moreover from instrs length have "0 < length phi" by simp
ultimately have "start!0 <=_r ?phi!0"
by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
moreover {
fix n'
have "OK None <=_r ?phi!n"
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
split: err.splits)
hence "\<lbrakk> n = Suc n'; n < size start \<rbrakk>
\<Longrightarrow> start!n <=_r ?phi!n" by simp
}
ultimately
show "n < size start \<Longrightarrow> start!n <=_r ?phi!n" by (cases n, blast+)
qed
moreover
from ck_type length
have "?phi \<in> list (size bs) A"
by (auto intro!: listI simp add: check_types_def)
moreover
from wt_err have "wt_step r Err step ?phi"
by (simp add: wt_err_step_def JVM_le_Err_conv)
ultimately
have "\<forall>p. p < size bs \<longrightarrow> kiljvm G C mxs mxr rT (mn=init) et bs start ! p \<noteq> Err"
by (unfold is_bcv_def) blast
with ck_bound instrs
show "wt_kil G C pTs rT (mn=init) mxs mxl et bs"
by (unfold wt_kil_def) (simp add: map_compose)
qed
theorem jvm_kildall_correct:
"wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)"
proof
let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in
SOME phi. wt_method G C (fst sig) (snd sig) rT maxs maxl ins et phi"
assume "wt_jvm_prog_kildall G"
hence "wt_jvm_prog G ?Phi"
apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
apply (erule jvm_prog_lift)
apply simp
apply (auto dest!: start_context.wt_kil_correct intro: someI)
done
thus "\<exists>Phi. wt_jvm_prog G Phi" by fast
next
assume "\<exists>Phi. wt_jvm_prog G Phi"
thus "wt_jvm_prog_kildall G"
apply (clarify)
apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
apply (erule jvm_prog_lift)
apply (auto intro: start_context.wt_kil_complete)
done
qed
end
theorem is_bcv_kiljvm:
[| wf_prog wf_mb G; is_class G C; set pTs <= types G;
bounded (Typing_Framework_JVM.exec G C mxs rT (mn = init) et bs)
(length bs) |]
==> is_bcv (JVMType.le G mxs (1 + length pTs + mxl)) Err
(Typing_Framework_JVM.exec G C mxs rT (mn = init) et bs) (length bs)
(states G mxs (1 + length pTs + mxl))
(kiljvm G C mxs (1 + length pTs + mxl) rT (mn = init) et bs)
lemma subset_replicate:
set (replicate n x) <= {x}
lemma in_set_replicate:
x : set (replicate n y) ==> x = y
lemma list_appendI:
[| a : list x A; b : list y A |] ==> a @ b : list (x + y) A
lemma start_in_A:
[| wf_prog wf_mb G; is_class G C; set pTs <= types G; 0 < length bs |]
==> OK (Some (([], OK (if mn = init & C ~= Object then PartInit C
else Init (Class C)) #
map (OK o Init) pTs @ replicate mxl Err),
C = Object)) #
replicate (length bs - 1) (OK None)
: list (length bs) (states G mxs (1 + length pTs + mxl))
theorem
[| wf_prog wf_mb G; is_class G C; set pTs <= types G;
wt_kil G C pTs rT (mn = init) mxs mxl et bs |]
==> EX phi. wt_method G C mn pTs rT mxs mxl bs et phi
theorem
[| wf_prog wf_mb G; is_class G C; set pTs <= types G;
wt_method G C mn pTs rT mxs mxl bs et phi |]
==> wt_kil G C pTs rT (mn = init) mxs mxl et bs
theorem jvm_kildall_correct:
wt_jvm_prog_kildall G = (EX Phi. wt_jvm_prog G Phi)