Up to index of Isabelle/HOL/arrays
theory JVM = Typing_Framework_JVM + Kildall:(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id: JVM.html,v 1.1 2002/11/28 16:11:18 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 \<equiv>
kildall (JVMType.le) (JVMType.sup) (exec G C maxs rT ini et bs)"
c_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> nat
\<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state list"
"c_kil G C pTs rT ini mxs mxl et bs \<equiv>
let this = OK (if ini \<and> C \<noteq> Object then PartInit C else Init (Class C));
first = (([],this#(map (OK\<circ>Init) pTs)@(replicate mxl Err)), C=Object);
start = OK {first}#(replicate (size bs - 1) (OK {}))
in kiljvm G C mxs (1+size pTs+mxl) rT ini et bs start"
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 bs \<equiv>
0 < size bs \<and> (\<forall>n < size bs. c_kil G C pTs rT ini mxs mxl et bs ! n \<noteq> Err)"
wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool"
"wt_jvm_prog_kildall G \<equiv>
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:
"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 (fold sl_def2, rule semilat_JVM)
apply (rule acc_JVM)
apply (simp add: JVMType.le_def)
apply (erule exec_pres_type)
apply (rule bounded_exec)
apply (erule exec_mono)
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 (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 states_def address_types_def init_tys_def max_dim_def)
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
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 c_kil_def) (simp add: map_compose)
have 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 (op \<subseteq>) step phi'"
by (simp add: wt_err_step_def JVMType.le_def)
from in_A have l: "size phi' = size bs" by simp
moreover {
from in_A have "check_types G mxs mxr (size bs) 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 (size bs) (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 JVMType.le_def Err.le_def)
}
moreover
have bounded: "bounded step (length bs) A" by simp (rule bounded_exec)
from in_A have "set phi' \<subseteq> A" by simp
with wt_err_step bounded
have "wt_app_eff (op \<subseteq>) app eff (map ok_val phi')"
by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def states_def)
ultimately
have "wt_method G C mn pTs rT mxs mxl bs et (map ok_val phi')"
using instrs 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_type: "check_types G mxs mxr (size bs) (map OK phi)" and
wt_start: "wt_start G C mn pTs mxl phi" and
app_eff: "wt_app_eff (op \<subseteq>) app eff phi"
by (simp add: wt_method_def2)
from ck_type
have in_A: "set (map OK phi) \<subseteq> A"
by (simp add: check_types_def)
have bounded: "bounded step (size bs) A"
by simp (rule bounded_exec)
with app_eff in_A
have "wt_err_step (op \<subseteq>) (err_step (size phi) app eff) (map OK phi)"
by - (erule wt_app_eff_imp_wt_err,
auto simp add: exec_def length states_def)
hence wt_err: "wt_err_step (op \<subseteq>) step (map OK phi)"
by (simp add: exec_def length)
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 "ok_val (start!0) \<subseteq> 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: JVMType.le_def Err.le_def lesub_def)
moreover {
fix n'
have "OK {} <=_r ?phi!n"
by (auto simp add: JVMType.le_def 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 JVMType.le_def)
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 instrs
show "wt_kil G C pTs rT (mn=init) mxs mxl et bs"
by (unfold c_kil_def 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"
-- "soundness"
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 (auto dest!: start_context.wt_kil_correct intro: someI)
done
thus "\<exists>Phi. wt_jvm_prog G Phi" by fast
next
-- "completeness"
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; Init ` set pTs <= init_tys G (length bs) |]
==> is_bcv JVMType.le Err
(Typing_Framework_JVM.exec G C mxs rT (mn = init) et bs) (length bs)
(states G mxs (1 + length pTs + mxl) (length bs))
(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 start_in_A:
[| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (length bs);
0 < length bs |]
==> OK {(([], 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 {})
: list (length bs) (states G mxs (1 + length pTs + mxl) (length bs))
theorem
[| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (length bs);
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; Init ` set pTs <= init_tys G (length bs);
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)