--- a/src/HOL/MicroJava/BV/JVM.thy Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Sun Mar 24 19:16:51 2002 +0100
@@ -102,13 +102,6 @@
lemmas [iff del] = not_None_eq
-lemma non_empty_succs: "succs i pc \<noteq> []"
- by (cases i) auto
-
-lemma non_empty:
- "non_empty (\<lambda>pc. eff (bs!pc) G pc et)"
- by (simp add: non_empty_def eff_def non_empty_succs)
-
theorem exec_pres_type:
"wf_prog wf_mb S \<Longrightarrow>
pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
@@ -391,12 +384,14 @@
by (clarsimp simp add: not_Err_eq)
from l bounded
- have bounded': "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
+ have "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
by (simp add: exec_def check_bounded_is_bounded)
+ hence bounded': "bounded (exec G maxs rT et bs) (length bs)"
+ by (auto intro: bounded_lift simp add: exec_def l)
with wt_err_step
have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et)
(\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
- by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def non_empty)
+ by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def)
with instrs l le bounded'
have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
apply (unfold wt_method_def wt_app_eff_def)
@@ -409,8 +404,9 @@
apply (erule allE, erule impE, assumption)
apply (elim conjE)
apply (clarsimp simp add: lesub_def wt_instr_def)
- apply (unfold bounded_def)
- apply blast
+ apply (simp add: exec_def)
+ apply (drule bounded_err_stepD, assumption+)
+ apply blast
done
thus ?thesis by blast
--- a/src/HOL/MicroJava/BV/Kildall_Lift.thy Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall_Lift.thy Sun Mar 24 19:16:51 2002 +0100
@@ -11,12 +11,6 @@
"app_mono r app n A ==
\<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"
-
-lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
- apply (induct xs)
- apply (auto simp add: map_snd_def)
- done
-
lemma bounded_lift:
"bounded step n \<Longrightarrow> bounded (err_step n app step) n"
apply (unfold bounded_def err_step_def error_def)
@@ -26,18 +20,6 @@
apply (auto simp add: map_snd_def split: split_if_asm)
done
-lemma boundedD2:
- "bounded (err_step n app step) n \<Longrightarrow>
- p < n \<Longrightarrow> app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow>
- q < n"
- apply (simp add: bounded_def err_step_def)
- apply (erule allE, erule impE, assumption)
- apply (erule_tac x = "OK a" in allE, drule bspec)
- apply (simp add: map_snd_def)
- apply fast
- apply simp
- done
-
lemma le_list_map_OK [simp]:
"\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
apply (induct a)
@@ -73,7 +55,7 @@
apply clarify
apply (drule in_map_sndD)
apply clarify
- apply (drule boundedD2, assumption+)
+ apply (drule bounded_err_stepD, assumption+)
apply (rule exI [of _ Err])
apply simp
apply simp
@@ -94,7 +76,7 @@
apply clarify
apply (drule in_map_sndD)
apply clarify
-apply (drule boundedD2, assumption+)
+apply (drule bounded_err_stepD, assumption+)
apply (rule exI [of _ Err])
apply simp
done
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Sun Mar 24 19:16:51 2002 +0100
@@ -18,70 +18,93 @@
"wt_app_eff r app step ts \<equiv>
\<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
+
map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list"
"map_snd f \<equiv> map (\<lambda>(x,y). (x, f y))"
error :: "nat \<Rightarrow> (nat \<times> 'a err) list"
"error n \<equiv> map (\<lambda>x. (x,Err)) [0..n(]"
+
err_step :: "nat \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
"err_step n app step p t \<equiv>
case t of
Err \<Rightarrow> error n
| OK t' \<Rightarrow> if app p t' then map_snd OK (step p t') else error n"
-non_empty :: "'s step_type \<Rightarrow> bool"
-"non_empty step \<equiv> \<forall>p t. step p t \<noteq> []"
-
-
lemmas err_step_defs = err_step_def map_snd_def error_def
-lemma non_emptyD:
- "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
-proof (unfold non_empty_def)
- assume "\<forall>p t. step p t \<noteq> []"
- hence "step p t \<noteq> []" by blast
- then obtain x xs where "step p t = x#xs"
- by (auto simp add: neq_Nil_conv)
- hence "x \<in> set(step p t)" by simp
- thus ?thesis by (cases x) blast
-qed
+lemma bounded_err_stepD:
+ "bounded (err_step n app step) n \<Longrightarrow>
+ p < n \<Longrightarrow> app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow>
+ q < n"
+ apply (simp add: bounded_def err_step_def)
+ apply (erule allE, erule impE, assumption)
+ apply (erule_tac x = "OK a" in allE, drule bspec)
+ apply (simp add: map_snd_def)
+ apply fast
+ apply simp
+ done
+
+
+lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
+ apply (induct xs)
+ apply (auto simp add: map_snd_def)
+ done
+lemma bounded_err_stepI:
+ "\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n))
+ \<Longrightarrow> bounded (err_step n ap step) n"
+apply (unfold bounded_def)
+apply clarify
+apply (simp add: err_step_def split: err.splits)
+apply (simp add: error_def)
+ apply blast
+apply (simp split: split_if_asm)
+ apply (blast dest: in_map_sndD)
+apply (simp add: error_def)
+apply blast
+done
+
+
+text {*
+ There used to be a condition here that each instruction must have a
+ successor. This is not needed any more, because the definition of
+ @{term error} trivially ensures that there is a successor for
+ the critical case where @{term app} does not hold.
+*}
lemma wt_err_imp_wt_app_eff:
- assumes b: "bounded step (size ts)"
- assumes n: "non_empty step"
assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
+ assumes b: "bounded (err_step (size ts) app step) (size ts)"
shows "wt_app_eff r app step (map ok_val ts)"
proof (unfold wt_app_eff_def, intro strip, rule conjI)
fix p assume "p < size (map ok_val ts)"
hence lp: "p < size ts" by simp
+ hence ts: "0 < size ts" by (cases p) auto
+ hence err: "(0,Err) \<in> set (error (size ts))" by (simp add: error_def)
from wt lp
have [intro?]: "\<And>p. p < size ts \<Longrightarrow> ts ! p \<noteq> Err"
by (unfold wt_err_step_def wt_step_def) simp
show app: "app p (map ok_val ts ! p)"
- proof -
- from wt lp
- obtain s where
+ proof (rule ccontr)
+ from wt lp obtain s where
OKp: "ts ! p = OK s" and
less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
by (unfold wt_err_step_def wt_step_def stable_def)
(auto iff: not_Err_eq)
-
- from n obtain q t where q: "(q,t) \<in> set(step p s)"
- by (blast dest: non_emptyD)
-
- from lp b q
- have lq: "q < size ts" by (unfold bounded_def) blast
- hence "ts!q \<noteq> Err" ..
- then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)
-
- with OKp less q lp have "app p s"
- by (auto simp add: err_step_defs split: err.split_asm split_if_asm)
-
- with lp OKp show ?thesis by simp
+ assume "\<not> app p (map ok_val ts ! p)"
+ with OKp lp have "\<not> app p s" by simp
+ with OKp have "err_step (size ts) app step p (ts!p) = error (size ts)"
+ by (simp add: err_step_def)
+ with err ts obtain q where
+ "(q,Err) \<in> set (err_step (size ts) app step p (ts!p))" and
+ q: "q < size ts" by auto
+ with less have "ts!q = Err" by auto
+ moreover from q have "ts!q \<noteq> Err" ..
+ ultimately show False by blast
qed
show "\<forall>(q,t)\<in>set(step p (map ok_val ts ! p)). t <=_r map ok_val ts ! q"
@@ -95,8 +118,7 @@
by (unfold wt_err_step_def wt_step_def stable_def)
(auto iff: not_Err_eq)
- from lp b q
- have lq: "q < size ts" by (unfold bounded_def) blast
+ from b lp app q have lq: "q < size ts" by (rule bounded_err_stepD)
hence "ts!q \<noteq> Err" ..
then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)
--- a/src/HOL/MicroJava/document/root.bib Sun Mar 24 14:06:21 2002 +0100
+++ b/src/HOL/MicroJava/document/root.bib Sun Mar 24 19:16:51 2002 +0100
@@ -66,3 +66,28 @@
note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
url = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}
}
+
+
+@article{KleinN-CPE01,
+ author = "Gerwin Klein and Tobias Nipow",
+ title = "Verified Lightweight Bytecode Verification",
+ journal = "Concurrency and Computation: Practice and Experience",
+ year = "2001",
+ volume = "13",
+ number = "13",
+ editor = "Gary T. Leavens and Susan Eisenbach",
+ pages = "1133-1151",
+ url = {http://www4.informatik.tu-muenchen.de/~kleing/papers/cpe01.html},
+ abstract = {Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual
+Machine code with types to enable a one-pass verification of welltypedness.
+We have formalized a variant of their proposal in the theorem prover
+Isabelle/HOL and proved soundness and completeness.},
+ note = {Invited contribution to special issue on Formal Techniques for Java},
+}
+
+
+@inproceedings{Nipkow-FOSSACS01,author={Tobias Nipkow},
+title={Verified Bytecode Verifiers},booktitle=
+{Foundations of Software Science and Computation Structures (FOSSACS 2001)},
+editor={F. Honsell},publisher=Springer,series=LNCS,volume=2030,
+pages={347--363},year=2001}