Up to index of Isabelle/HOL/arrays
theory LBVJVM = LBVCorrect + LBVComplete + Typing_Framework_JVM:(* Title: HOL/MicroJava/BV/LBVJVM.thy
ID: $Id: LBVJVM.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
header {* \isaheader{LBV for the JVM}\label{sec:JVM} *}
theory LBVJVM = LBVCorrect + LBVComplete + Typing_Framework_JVM:
types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> state list"
constdefs
check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
"check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr n cert \<and> length cert = n+1 \<and>
(\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK {}"
lbvjvm :: "jvm_prog \<Rightarrow> cname \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> exception_table \<Rightarrow>
state list \<Rightarrow> instr list \<Rightarrow> state \<Rightarrow> state"
"lbvjvm G C maxs maxr rT ini et cert bs \<equiv>
wtl_inst_list bs cert JVMType.sup JVMType.le Err (OK {}) (exec G C maxs rT ini et bs) 0"
wt_lbv :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
exception_table \<Rightarrow> state list \<Rightarrow> instr list \<Rightarrow> bool"
"wt_lbv G C mn pTs rT mxs mxl et cert ins \<equiv>
check_cert G mxs (1+size pTs+mxl) (length ins) cert \<and>
0 < size ins \<and>
(let this = OK (if mn=init \<and> C \<noteq> Object then PartInit C else Init (Class C));
start = {(([],this#(map (OK\<circ>Init) pTs)@(replicate mxl Err)),C=Object)};
result = lbvjvm G C mxs (1+size pTs+mxl) rT (mn=init) et cert ins (OK start)
in result \<noteq> Err)"
wt_jvm_prog_lbv :: "jvm_prog \<Rightarrow> prog_cert \<Rightarrow> bool"
"wt_jvm_prog_lbv G cert \<equiv>
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_lbv G C (fst sig) (snd sig) rT maxs maxl et (cert C sig) b) G"
mk_cert :: "jvm_prog \<Rightarrow> cname \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> exception_table \<Rightarrow> instr list
\<Rightarrow> method_type \<Rightarrow> state list"
"mk_cert G C maxs rT ini et bs phi \<equiv> make_cert (exec G C maxs rT ini et bs) (map OK phi) (OK {})"
prg_cert :: "jvm_prog \<Rightarrow> prog_type \<Rightarrow> prog_cert"
"prg_cert G phi C sig \<equiv> let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in
mk_cert G C maxs rT (fst sig=init) et ins (phi C sig)"
lemma check_certD:
"check_cert G mxs mxr n cert \<Longrightarrow> cert_ok cert n Err (OK {}) (states G mxs mxr n)"
by (unfold cert_ok_def check_cert_def check_types_def) auto
lemma (in start_context) first_in_A: "OK {first} \<in> A"
apply (insert pTs C)
apply (simp add: states_def address_types_def init_tys_def max_dim_def)
apply (auto intro!: list_appendI)
apply force+
done
lemma (in start_context) wt_lbv_wt_step:
assumes lbv: "wt_lbv G C mn pTs rT mxs mxl et cert bs"
defines [simp]: "f \<equiv> JVMType.sup"
shows "\<exists>ts \<in> list (size bs) A. wt_step r Err step ts \<and> OK {first} <=_r ts!0"
proof -
have "semilat (JVMType.sl G mxs mxr (size bs))" by (rule semilat_JVM)
hence "semilat (A, r, f)" by (simp add: sl_def2)
moreover
have "top r Err" by (simp add: JVMType.le_def)
moreover
have "Err \<in> A" by (simp add: states_def)
moreover
have "bottom r (OK {})"
by (simp add: JVMType.le_def bottom_def lesub_def Err.le_def split: err.split)
moreover
have "OK {} \<in> A" by (simp add: states_def)
moreover
have "bounded step (length bs) A" by (simp add: bounded_exec)
moreover
from lbv
have "cert_ok cert (length bs) Err (OK {}) A"
by (unfold wt_lbv_def) (auto dest: check_certD)
moreover
from wf
have "pres_type step (length bs) A" by simp (rule exec_pres_type)
moreover
from lbv
have "wtl_inst_list bs cert f r Err (OK {}) step 0 (OK {first}) \<noteq> Err"
by (simp add: wt_lbv_def lbvjvm_def)
moreover
note first_in_A
moreover
from lbv have "0 < length bs" by (simp add: wt_lbv_def)
ultimately
show ?thesis by (rule lbvs.wtl_sound_strong)
qed
lemma in_list:
"(xs \<in> list n A) = (length xs = n \<and> set xs \<subseteq> A)"
by (unfold list_def) auto
lemma (in start_context) wt_lbv_wt_method:
assumes lbv: "wt_lbv G C mn pTs rT mxs mxl et cert bs"
shows "\<exists>phi. wt_method G C mn pTs rT mxs mxl bs et phi"
proof -
from lbv have l: "bs \<noteq> []" by (simp add: wt_lbv_def)
moreover
from wf lbv C pTs
obtain phi where
list: "phi \<in> list (length bs) A" and
step: "wt_step r Err step phi" and
start: "OK {first} <=_r phi!0"
by (blast dest: wt_lbv_wt_step)
from list have [simp]: "length phi = length bs" by simp
have "length (map ok_val phi) = length bs" by simp
moreover
from l have 0: "0 < length phi" by simp
with step obtain phi0 where "phi!0 = OK phi0"
by (unfold wt_step_def) blast
with start 0
have "wt_start G C mn pTs mxl (map ok_val phi)"
by (simp add: wt_start_def JVMType.le_def lesub_def map_compose Err.le_def)
moreover {
from list
have "check_types G mxs mxr (length bs) phi"
by (simp add: check_types_def)
also from step
have [symmetric]: "map OK (map ok_val phi) = phi"
by (auto intro!: map_id simp add: wt_step_def)
finally have "check_types G mxs mxr (length bs) (map OK (map ok_val phi))" .
}
moreover {
have "bounded (err_step (length phi) app eff) (length bs) A"
by (simp, fold exec_def) (rule bounded_exec)
moreover
from list have "set phi \<subseteq> A" by simp
moreover
from step
have "wt_err_step (op \<subseteq>) step phi"
by (simp add: wt_err_step_def JVMType.le_def)
ultimately
have "wt_app_eff (op \<subseteq>) app eff (map ok_val phi)"
by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def states_def)
}
ultimately
have "wt_method G C mn pTs rT mxs mxl bs et (map ok_val phi)"
by (simp add: wt_method_def2)
thus ?thesis ..
qed
lemma (in start_context) wt_method_wt_lbv:
assumes wt: "wt_method G C mn pTs rT mxs mxl bs et phi"
defines [simp]: "cert \<equiv> mk_cert G C mxs rT (mn=init) et bs phi"
defines [simp]: "f \<equiv> JVMType.sup"
shows "wt_lbv G C mn pTs rT mxs mxl et cert bs"
proof -
let ?phi = "map OK phi"
let ?cert = "make_cert step ?phi (OK {})"
from wt obtain
0: "0 < length bs" and
length: "length bs = length ?phi" and
ck_types: "check_types G mxs mxr (length bs) ?phi" and
wt_start: "wt_start G C mn pTs mxl phi" and
app_eff: "wt_app_eff (op \<subseteq>) app eff phi"
by (force simp add: wt_method_def2)
have "semilat (JVMType.sl G mxs mxr (size bs))" by (rule semilat_JVM)
hence "semilat (A, r, f)" by (simp add: sl_def2)
moreover
have "top r Err" by (simp add: JVMType.le_def)
moreover
have "Err \<in> A" by (simp add: states_def)
moreover
have "bottom r (OK {})"
by (simp add: JVMType.le_def bottom_def Err.le_def lesub_def split: err.splits)
moreover
have "OK {} \<in> A" by (simp add: states_def)
moreover
have bounded: "bounded step (length bs) A" by (simp add: bounded_exec)
with wf
have "mono r step (length bs) A" by simp (rule exec_mono)
hence "mono r step (length ?phi) A" by (simp add: length)
moreover
from wf have "pres_type step (length bs) A" by simp (rule exec_pres_type)
hence "pres_type step (length ?phi) A" by (simp add: length)
moreover
from ck_types
have phi_in_A: "set ?phi \<subseteq> A" by (simp add: check_types_def)
hence "\<forall>pc. pc < length ?phi \<longrightarrow> ?phi!pc \<in> A \<and> ?phi!pc \<noteq> Err" by auto
moreover
from bounded
have "bounded step (length ?phi) A" by (simp add: length)
moreover
have "OK {} \<noteq> Err" by simp
moreover
from bounded length phi_in_A app_eff
have "wt_err_step (op \<subseteq>) step ?phi"
by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def states_def)
hence "wt_step r Err step ?phi"
by (simp add: wt_err_step_def JVMType.le_def)
moreover
from 0 length have "0 < length phi" by auto
hence "?phi!0 = OK (phi!0)" by simp
with wt_start have "OK {first} <=_r ?phi!0"
by (clarsimp simp add: wt_start_def lesub_def Err.le_def JVMType.le_def map_compose)
moreover
note first_in_A
moreover
have "OK {first} \<noteq> Err" by simp
moreover
note length
ultimately
have "wtl_inst_list bs ?cert f r Err (OK {}) step 0 (OK {first}) \<noteq> Err"
by (rule lbvc.wtl_complete)
moreover
from 0 length have "phi \<noteq> []" by auto
moreover
from ck_types
have "check_types G mxs mxr (length bs) ?cert"
by (force simp add: make_cert_def check_types_def states_def)
moreover
note 0 length
ultimately
show ?thesis by (simp add: wt_lbv_def lbvjvm_def mk_cert_def
check_cert_def make_cert_def nth_append)
qed
theorem jvm_lbv_correct:
"wt_jvm_prog_lbv G Cert \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
proof -
let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,bs,et)) = the (method (G,C) sig) in
SOME phi. wt_method G C (fst sig) (snd sig) rT maxs maxl bs et phi"
assume "wt_jvm_prog_lbv G Cert"
hence "wt_jvm_prog G ?Phi"
apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
apply (erule jvm_prog_lift)
apply (auto dest!: start_context.wt_lbv_wt_method intro: someI)
done
thus ?thesis by blast
qed
theorem jvm_lbv_complete:
"wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)"
apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
apply (erule jvm_prog_lift)
apply (auto simp add: prg_cert_def intro: start_context.wt_method_wt_lbv)
done
end
lemma check_certD:
check_cert G mxs mxr n cert ==> cert_ok cert n Err (OK {}) (states G mxs mxr n)
lemma first_in_A:
[| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (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)}
: states G mxs (1 + length pTs + mxl) (length bs)
lemma
[| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (length bs);
wt_lbv G C mn pTs rT mxs mxl et cert bs |]
==> EX ts:list (length bs) (states G mxs (1 + length pTs + mxl) (length bs)).
wt_step JVMType.le Err
(Typing_Framework_JVM.exec G C mxs rT (mn = init) et bs) ts &
OK {(([], OK (if mn = init & C ~= Object then PartInit C
else Init (Class C)) #
map (OK o Init) pTs @ replicate mxl Err),
C = Object)}
<=_JVMType.le ts ! 0
lemma in_list:
(xs : list n A) = (length xs = n & set xs <= A)
lemma
[| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (length bs);
wt_lbv G C mn pTs rT mxs mxl et cert bs |]
==> EX phi. wt_method G C mn pTs rT mxs mxl bs et phi
lemma
[| 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_lbv G C mn pTs rT mxs mxl et (mk_cert G C mxs rT (mn = init) et bs phi)
bs
theorem jvm_lbv_correct:
wt_jvm_prog_lbv G Cert ==> EX Phi. wt_jvm_prog G Phi
theorem jvm_lbv_complete:
wt_jvm_prog G Phi ==> wt_jvm_prog_lbv G (prg_cert G Phi)