Up to index of Isabelle/HOL/objinit
theory LBVJVM = LBVCorrect + LBVComplete + Typing_Framework_JVM:(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id: LBVJVM.html,v 1.1 2002/11/28 14:12:09 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 cert \<and> length cert = n+1 \<and>
(\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None"
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 G maxs maxr) (JVMType.le G maxs maxr) Err (OK None) (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_bounded ins et \<and>
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 = Some (([],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 None)"
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 None) (states G mxs mxr)"
apply (unfold cert_ok_def check_cert_def check_types_def)
apply (auto simp add: list_all_ball)
done
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 list_map [simp]:
"(map f xs \<in> list (length xs) A) = (f ` set xs \<subseteq> A)"
apply (unfold list_def)
apply simp
done
lemma [intro]:
"x \<in> A \<Longrightarrow> replicate n x \<in> list n A"
by (induct n, auto)
lemma (in start_context) first_in_A: "OK first \<in> A"
apply (insert pTs C)
apply (simp add: JVM_states_unfold)
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 G mxs mxr"
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)" by (rule semilat_JVM_slI)
hence "semilat (A, r, f)" by (simp add: sl_triple_conv)
moreover
have "top r Err" by (simp add: JVM_le_unfold)
moreover
have "Err \<in> A" by (simp add: JVM_states_unfold)
moreover
have "bottom r (OK None)"
by (simp add: JVM_le_unfold bottom_def)
moreover
have "OK None \<in> A" by (simp add: JVM_states_unfold)
moreover
from lbv
have "bounded step (length bs)"
by (clarsimp simp add: wt_lbv_def exec_def)
(intro bounded_lift check_bounded_is_bounded)
moreover
from lbv
have "cert_ok cert (length bs) Err (OK None) A"
by (unfold wt_lbv_def) (auto dest: check_certD)
moreover
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 None) 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 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 JVM_le_Err_conv lesub_def map_compose)
moreover
from lbv have chk_bounded: "check_bounded bs et"
by (simp add: wt_lbv_def)
moreover {
from list
have "check_types G mxs mxr 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 (map OK (map ok_val phi))" .
}
moreover {
from chk_bounded
have "bounded (err_step (length bs) app eff) (length bs)"
by simp (blast intro: bounded_lift check_bounded_is_bounded)
moreover
from step
have "wt_err_step (sup_state_opt G) step phi"
by (simp add: wt_err_step_def JVM_le_Err_conv)
ultimately
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: exec_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 G mxs mxr"
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 None)"
from wt obtain
0: "0 < length bs" and
length: "length bs = length ?phi" and
ck_bounded: "check_bounded bs et" and
ck_types: "check_types G mxs mxr ?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 (force simp add: wt_method_def2)
have "semilat (JVMType.sl G mxs mxr)" by (rule semilat_JVM_slI)
hence "semilat (A, r, f)" by (simp add: sl_triple_conv)
moreover
have "top r Err" by (simp add: JVM_le_unfold)
moreover
have "Err \<in> A" by (simp add: JVM_states_unfold)
moreover
have "bottom r (OK None)"
by (simp add: JVM_le_unfold bottom_def)
moreover
have "OK None \<in> A" by (simp add: JVM_states_unfold)
moreover
from ck_bounded
have bounded: "bounded step (length bs)"
by (clarsimp simp add: exec_def)
(intro bounded_lift check_bounded_is_bounded)
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
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 "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)" by (simp add: length)
moreover
have "OK None \<noteq> Err" by simp
moreover
from bounded length app_eff
have "wt_err_step (sup_state_opt G) step ?phi"
by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def)
hence "wt_step r Err step ?phi"
by (simp add: wt_err_step_def JVM_le_Err_conv)
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 JVM_le_Err_conv 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 None) 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 ?cert"
by (auto simp add: make_cert_def check_types_def JVM_states_unfold)
moreover
note ck_bounded 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 None) (states G mxs mxr)
lemma list_appendI:
[| a : list x A; b : list y A |] ==> a @ b : list (x + y) A
lemma list_map:
(map f xs : list (length xs) A) = (f ` set xs <= A)
lemma
x : A ==> replicate n x : list n A
lemma first_in_A:
[| wf_prog wf_mb G; is_class G C; set pTs <= types G |]
==> 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))
: states G mxs (1 + length pTs + mxl)
lemma
[| wf_prog wf_mb G; is_class G C; set pTs <= types G;
wt_lbv G C mn pTs rT mxs mxl et cert bs |]
==> EX ts:list (length bs) (states G mxs (1 + length pTs + mxl)).
wt_step (JVMType.le G mxs (1 + length pTs + mxl)) Err
(Typing_Framework_JVM.exec G C mxs rT (mn = init) et bs) ts &
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))
<=_(JVMType.le G mxs (1 + length pTs + mxl)) ts ! 0
lemma
[| wf_prog wf_mb G; is_class G C; set pTs <= types G;
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; set pTs <= types G;
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)