Up to index of Isabelle/HOL/objinit
theory BVExample = JVMListExample + BVSpecTypeSafe:(* Title: HOL/MicroJava/BV/BVExample.thy
ID: $Id: BVExample.html,v 1.1 2002/11/28 14:12:09 kleing Exp $
Author: Gerwin Klein
*)
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
theory BVExample = JVMListExample + BVSpecTypeSafe:
text {*
This theory shows type correctness of the example program in section
\ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
explicitly providing a welltyping. It also shows that the start
state of the program conforms to the welltyping; hence type safe
execution is guaranteed.
*}
section "Setup"
text {*
Since the types @{typ cnam}, @{text vnam}, and @{text mname} are
anonymous, we describe distinctness of names in the example by axioms:
*}
axioms
distinct_classes [simp]: "list_nam \<noteq> test_nam"
distinct_fields [simp]: "val_nam \<noteq> next_nam"
distinct_meth_list [simp]: "append_name \<noteq> init"
distinct_meth_test [simp]: "makelist_name \<noteq> init"
declare
distinct_classes [symmetric, simp]
distinct_fields [symmetric, simp]
distinct_meth_list [symmetric, simp]
distinct_meth_test [symmetric, simp]
text {* Abbreviations for theorem sets we will have to use often in the
proofs below: *}
lemmas name_defs = list_name_def test_name_def val_name_def next_name_def
lemmas system_defs = JVMSystemClasses_def SystemClassC_defs
lemmas class_defs = list_class_def test_class_def
text {* These auxiliary proofs are for efficiency: class lookup,
subclass relation, method and field lookup are computed only once:
*}
lemma class_Object [simp]:
"class E Object = Some (arbitrary, [],[Object_ctor])"
by (simp add: class_def system_defs E_def)
lemma class_NullPointer [simp]:
"class E (Xcpt NullPointer) = Some (Object, [], [Default_ctor])"
by (simp add: class_def system_defs E_def)
lemma class_OutOfMemory [simp]:
"class E (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])"
by (simp add: class_def system_defs E_def)
lemma class_ClassCast [simp]:
"class E (Xcpt ClassCast) = Some (Object, [], [Default_ctor])"
by (simp add: class_def system_defs E_def)
lemma class_list [simp]:
"class E list_name = Some list_class"
by (simp add: class_def system_defs E_def name_defs)
lemma class_test [simp]:
"class E test_name = Some test_class"
by (simp add: class_def system_defs E_def name_defs)
lemma E_classes [simp]:
"{C. is_class E C} = {list_name, test_name, Xcpt NullPointer,
Xcpt ClassCast, Xcpt OutOfMemory, Object}"
by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
text {* The subclass releation spelled out: *}
lemma subcls1:
"subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
apply (simp add: subcls1_def2)
apply (simp add: name_defs class_defs system_defs E_def class_def)
apply (auto split: split_if_asm)
done
text {* The subclass relation is acyclic; hence its converse is well founded: *}
lemma notin_rtrancl:
"(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
by (auto elim: converse_rtranclE)
lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
apply (rule acyclicI)
apply (simp add: subcls1)
apply (auto dest!: tranclD)
apply (auto elim!: notin_rtrancl simp add: name_defs)
done
lemma wf_subcls1_E: "wf ((subcls1 E)¯)"
apply (rule finite_acyclic_wf_converse)
apply (simp add: subcls1)
apply (rule acyclic_subcls1_E)
done
text {* Method and field lookup: *}
lemma method_Object [simp]:
"method (E, Object) sig =
(if sig = (init,[]) then
Some (Object, PrimT Void, Suc 0, 0, [LitPush Unit, Return], [])
else None)"
by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E] Object_ctor_def)
lemma method_append [simp]:
"method (E, list_name) (append_name, [Class list_name]) =
Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
apply (insert class_list)
apply (unfold list_class_def)
apply (drule method_rec_lemma [OF _ wf_subcls1_E])
apply (simp add: name_defs Default_ctor_def)
done
lemma method_makelist [simp]:
"method (E, test_name) (makelist_name, []) =
Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
apply (insert class_test)
apply (unfold test_class_def)
apply (drule method_rec_lemma [OF _ wf_subcls1_E])
apply (simp add: name_defs Default_ctor_def)
done
lemma method_default_ctor [simp]:
"method (E, list_name) (init, []) =
Some (list_name,PrimT Void,1,0,[Load 0,Invoke_special Object init [],Return],[])"
apply (insert class_list)
apply (unfold list_class_def)
apply (drule method_rec_lemma [OF _ wf_subcls1_E])
apply (simp add: name_defs Default_ctor_def)
done
lemma field_val [simp]:
"field (E, list_name) val_name = Some (list_name, PrimT Integer)"
apply (unfold field_def)
apply (insert class_list)
apply (unfold list_class_def)
apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
apply simp
done
lemma field_next [simp]:
"field (E, list_name) next_name = Some (list_name, Class list_name)"
apply (unfold field_def)
apply (insert class_list)
apply (unfold list_class_def)
apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
apply (simp add: name_defs distinct_fields [symmetric])
done
lemma [simp]: "fields (E, Object) = []"
by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
lemma [simp]: "fields (E, Xcpt NullPointer) = []"
by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
lemma [simp]: "fields (E, Xcpt ClassCast) = []"
by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
lemma [simp]: "fields (E, test_name) = []"
apply (insert class_test)
apply (unfold test_class_def)
apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
apply simp
done
lemmas [simp] = is_class_def
text {*
The next definition and three proof rules implement an algorithm to
enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"}
transforms a goal of the form
@{prop [display] "pc < n \<Longrightarrow> P pc"}
into a series of goals
@{prop [display] "P 0"}
@{prop [display] "P (Suc 0)"}
@{text "\<dots>"}
@{prop [display] "P n"}
*}
constdefs
intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")
"x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
by (simp add: intervall_def)
lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
apply (cases "x=n0")
apply (auto simp add: intervall_def)
done
lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x"
by (unfold intervall_def) arith
section "Program structure"
text {*
The program is structurally wellformed:
*}
lemma wf_struct:
"wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
proof -
note simps [simp] = wf_mdecl_def wf_mhead_def wf_cdecl_def system_defs
have "unique E"
by (simp add: E_def class_defs name_defs)
moreover
have "set JVMSystemClasses \<subseteq> set E" by (simp add: E_def)
hence "wf_syscls E" by (rule wf_syscls)
moreover
have "wf_cdecl ?mb E ObjectC" by simp
moreover
have "wf_cdecl ?mb E NullPointerC"
by (auto elim: notin_rtrancl simp add: name_defs subcls1)
moreover
have "wf_cdecl ?mb E ClassCastC"
by (auto elim: notin_rtrancl simp add: name_defs subcls1)
moreover
have "wf_cdecl ?mb E OutOfMemoryC"
by (auto elim: notin_rtrancl simp add: name_defs subcls1)
moreover
have "wf_cdecl ?mb E (list_name, list_class)"
apply (auto elim!: notin_rtrancl
simp add: wf_fdecl_def list_class_def subcls1)
apply (auto simp add: name_defs)
done
moreover
have "wf_cdecl ?mb E (test_name, test_class)"
apply (auto elim!: notin_rtrancl
simp add: wf_fdecl_def test_class_def subcls1)
apply (auto simp add: name_defs)
done
ultimately
show ?thesis by (simp del: simps add: wf_prog_def E_def JVMSystemClasses_def)
qed
section "Welltypings"
text {*
We show welltypings of all methods in the program @{text E}.
The more interesting ones are @{term append_name} in class @{term list_name},
and @{term makelist_name} in class @{term test_name}. The rest are
default constructors.
*}
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def eff_bool_def subtype_def
declare
appInvoke [simp del]
appInvoke_special [simp del]
constdefs
phi_obj_ctor :: method_type ("\<phi>\<^sub>o")
"\<phi>\<^sub>o \<equiv> [Some (([], [OK (Init (Class Object))]), True),
Some (([Init (PrimT Void)], [OK (Init (Class Object))]), True)]"
section {* Executability of @{term check_bounded} *}
consts
list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
primrec
"list_all'_rec P n [] = True"
"list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
constdefs
list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
"list_all' P xs \<equiv> list_all'_rec P 0 xs"
lemma list_all'_rec:
"\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
apply (induct xs)
apply auto
apply (case_tac p)
apply auto
done
lemma list_all':
"list_all' P xs = (\<forall>n < size xs. P (xs!n) n)"
by (unfold list_all'_def) (simp add: list_all'_rec)
lemma list_all_ball:
"list_all P xs = (\<forall>x \<in> set xs. P x)"
by (induct xs) auto
lemma [simp]:
"check_bounded ins et =
(list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and>
list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
by (simp add: list_all_ball list_all' check_bounded_def)
declare list_all'_def [simp]
lemma init_tys_def2 [simp]:
"init_tys E = {Init y | y. is_type E y} \<union> {UnInit c n | c n. True} \<union> {PartInit c | c. True}"
apply (unfold init_tys_def JType.esl_def)
apply auto
done
lemma check_types_lemma [simp]:
"b \<in> list mxr (err (init_tys E)) \<Longrightarrow>
a \<in> list (length a) (init_tys E) \<Longrightarrow>
length a \<le> mxs \<Longrightarrow>
OK (Some ((a, b), x)) \<in> states E mxs mxr"
apply (unfold states_def)
apply (unfold JVMType.sl_def)
apply (unfold Err.sl_def Err.esl_def Opt.esl_def Product.esl_def
stk_esl_def reg_sl_def TrivLat.esl_def upto_esl_def Listn.sl_def
Init.esl_def)
apply (simp (no_asm) del: init_tys_def2)
apply blast
done
lemma Object_init [simp]:
"wt_method E Object init [] (PrimT Void) (Suc 0) 0 [LitPush Unit, Return] [] \<phi>\<^sub>o"
apply (simp add: wt_method_def phi_obj_ctor_def
wt_start_def wt_instr_def)
apply (simp add: check_types_def)
apply clarify
apply (elim pc_end pc_next pc_0)
apply fastsimp
apply fastsimp
done
constdefs
phi_default_ctor :: "cname \<Rightarrow> method_type" ("\<phi>\<^sub>c _")
"\<phi>\<^sub>c C \<equiv> [Some (([], [OK (PartInit C)]), False),
Some (([PartInit C], [OK (PartInit C)]), False),
Some (([Init (PrimT Void)], [OK (Init (Class C))]), True)]"
lemma [simp]: "Ex Not" by fast
lemma [simp]: "\<exists>z. z" by fast
lemma default_ctor [simp]:
"E \<turnstile> C \<prec>C1 Object \<Longrightarrow> is_class E C \<Longrightarrow>
wt_method E C init [] (PrimT Void) (Suc 0) 0
[Load 0, Invoke_special Object init [], Return] [] (\<phi>\<^sub>c C)"
apply (simp add: wt_method_def phi_default_ctor_def
wt_start_def wt_instr_def check_types_def)
apply (rule conjI)
apply clarify
apply (elim pc_end pc_next pc_0)
apply simp
apply (simp add: app_def xcpt_app_def replace_def)
apply simp
apply (fast dest: subcls1_wfD [OF _ wf_struct])
done
constdefs
phi_append :: method_type ("\<phi>\<^sub>a")
"\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some ((map Init x, map (OK \<circ> Init) y), False)) [
( [], [Class list_name, Class list_name]),
( [Class list_name], [Class list_name, Class list_name]),
( [Class list_name], [Class list_name, Class list_name]),
( [Class list_name, Class list_name], [Class list_name, Class list_name]),
([NT, Class list_name, Class list_name], [Class list_name, Class list_name]),
( [Class list_name], [Class list_name, Class list_name]),
( [Class list_name, Class list_name], [Class list_name, Class list_name]),
( [PrimT Void], [Class list_name, Class list_name]),
( [Class Object], [Class list_name, Class list_name]),
( [], [Class list_name, Class list_name]),
( [Class list_name], [Class list_name, Class list_name]),
( [Class list_name, Class list_name], [Class list_name, Class list_name]),
( [], [Class list_name, Class list_name]),
( [PrimT Void], [Class list_name, Class list_name])]"
lemma wt_append [simp]:
"wt_method E list_name append_name [Class list_name] (PrimT Void) 3 0 append_ins
[(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
apply (simp add: wt_method_def append_ins_def phi_append_def
wt_start_def wt_instr_def name_defs)
apply (fold name_defs)
apply (simp add: check_types_def)
apply clarify
apply (elim pc_end pc_next pc_0)
apply simp
apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
apply simp
apply simp
apply (fastsimp simp add: sup_state_conv subcls1)
apply simp
apply (simp add: app_def xcpt_app_def)
apply simp
apply simp
apply simp
apply simp
apply (simp add: match_exception_entry_def)
apply simp
apply simp
done
text {* Some abbreviations for readability *}
syntax
list :: ty
test :: ty
intg :: ty
void :: ty
translations
"list" == "Init (Class list_name)"
"test" == "Init (Class test_name)"
"intg" == "Init (PrimT Integer)"
"void" == "Init (PrimT Void)"
constdefs
phi_makelist :: method_type ("\<phi>\<^sub>m")
"\<phi>\<^sub>m \<equiv> map (\<lambda>x. Some (x,False)) [
( [], [OK test, Err, Err]),
( [UnInit list_name 0], [OK test, Err, Err]),
( [UnInit list_name 0, UnInit list_name 0], [OK test, Err, Err]),
([UnInit list_name 0,UnInit list_name 0,UnInit list_name 0],[OK test,Err,Err]),
( [void, list, list], [OK test, Err, Err]),
( [list, list], [OK test, Err, Err]),
( [list], [OK list, Err, Err]),
( [intg, list], [OK list, Err, Err]),
( [], [OK list, Err, Err]),
( [UnInit list_name 8], [OK list, Err, Err]),
( [UnInit list_name 8, UnInit list_name 8], [OK list, Err, Err]),
( [void, list], [OK list, Err, Err]),
( [list], [OK list, Err, Err]),
( [list, list], [OK list, Err, Err]),
( [list], [OK list, OK list, Err]),
( [intg, list], [OK list, OK list, Err]),
( [], [OK list, OK list, Err]),
( [UnInit list_name 16], [OK list, OK list, Err]),
( [UnInit list_name 16, UnInit list_name 16], [OK list, OK list, Err]),
( [void, list], [OK list, OK list, Err]),
( [list], [OK list, OK list, Err]),
( [list, list], [OK list, OK list, Err]),
( [list], [OK list, OK list, OK list]),
( [intg, list], [OK list, OK list, OK list]),
( [], [OK list, OK list, OK list]),
( [list], [OK list, OK list, OK list]),
( [list, list], [OK list, OK list, OK list]),
( [void], [OK list, OK list, OK list]),
( [list, void], [OK list, OK list, OK list]),
( [list, list, void], [OK list, OK list, OK list]),
( [void, void], [OK list, OK list, OK list])
]"
lemma wt_makelist [simp]:
"wt_method E test_name makelist_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
apply (simp add: wt_start_def nat_number)
apply (simp add: wt_instr_def name_defs)
apply (fold name_defs)
apply (simp add: check_types_def)
apply clarify
apply (elim pc_end pc_next pc_0)
apply (simp add: replace_def)
apply simp
apply simp
apply (simp add: app_def xcpt_app_def replace_def)
apply simp
apply simp
apply simp
apply simp
apply (simp add: replace_def)
apply simp
apply simp
apply (simp add: app_def xcpt_app_def replace_def)
apply simp
apply simp
apply simp
apply simp
apply simp
apply (simp add: replace_def)
apply simp
apply simp
apply (simp add: app_def xcpt_app_def replace_def)
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
apply (simp add: app_def xcpt_app_def)
apply simp
apply simp
apply (simp add: app_def xcpt_app_def)
apply simp
done
text {* The whole program is welltyped: *}
constdefs
Phi :: prog_type ("\<Phi>")
"\<Phi> C sig \<equiv> if C = Object \<and> sig = (init,[]) then \<phi>\<^sub>o else
if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else
if sig = (init,[]) then \<phi>\<^sub>c C else []"
lemma [simp]:
"is_class E C =
(C \<in> {Cname list_nam, Cname test_nam, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory, Object})"
apply (insert E_classes)
apply (auto simp add: name_defs)
done
declare is_class_def [simp del]
lemma wf_prog:
"wt_jvm_prog E \<Phi>"
apply (unfold wt_jvm_prog_def)
apply (rule wf_mb'E [OF wf_struct])
apply (simp add: E_def)
apply clarify
apply (fold E_def)
apply (simp add: system_defs class_defs)
apply auto
apply (auto simp add: Phi_def)
apply (insert subcls1)
apply (auto simp add: name_defs)
done
section "Conformance"
text {* Execution of the program will be typesafe, because its
start state conforms to the welltyping: *}
lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"
apply (rule BV_correct_initial)
apply (rule wf_prog)
apply (auto simp add: is_class_def)
done
end
lemmas name_defs:
list_name == Cname list_nam
test_name == Cname test_nam
val_name == VName val_nam
next_name == VName next_nam
lemmas system_defs:
JVMSystemClasses == [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]
ObjectC_decl ms == (Object, arbitrary, [], ms)
NullPointerC_decl ms == (Xcpt NullPointer, Object, [], ms)
ClassCastC_decl ms == (Xcpt ClassCast, Object, [], ms)
OutOfMemoryC_decl ms == (Xcpt OutOfMemory, Object, [], ms)
ObjectC == ObjectC_decl [Object_ctor]
NullPointerC == NullPointerC_decl [Default_ctor]
OutOfMemoryC == OutOfMemoryC_decl [Default_ctor]
ClassCastC == ClassCastC_decl [Default_ctor]
Default_ctor == ((init, []), PrimT Void, 1, 0, [Load 0, Invoke_special Object init [], Return], [])
Object_ctor == ((init, []), PrimT Void, 1, 0, [LitPush Unit, Return], [])
lemmas class_defs:
list_class ==
(Object, [(val_name, PrimT Integer), (next_name, Class list_name)],
[Default_ctor,
((append_name, [Class list_name]), PrimT Void, 3, 0, append_ins,
[(1, 2, 8, Xcpt NullPointer)])])
test_class == (Object, [], [Default_ctor, ((makelist_name, []), PrimT Void, 3, 2, make_list_ins, [])])
lemma class_Object:
class E Object = Some (arbitrary, [], [Object_ctor])
lemma class_NullPointer:
class E (Xcpt NullPointer) = Some (Object, [], [Default_ctor])
lemma class_OutOfMemory:
class E (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])
lemma class_ClassCast:
class E (Xcpt ClassCast) = Some (Object, [], [Default_ctor])
lemma class_list:
class E list_name = Some list_class
lemma class_test:
class E test_name = Some test_class
lemma E_classes:
Collect (is_class E) =
{list_name, test_name, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory,
Object}
lemma subcls1:
subcls1 E =
{(list_name, Object), (test_name, Object), (Xcpt NullPointer, Object),
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}
lemma notin_rtrancl:
[| (a, b) : r^*; a ~= b; !!y. (a, y) ~: r |] ==> False
lemma acyclic_subcls1_E:
acyclic (subcls1 E)
lemma wf_subcls1_E:
wf ((subcls1 E)^-1)
lemma method_Object:
method (E, Object) sig = (if sig = (init, []) then Some (Object, PrimT Void, Suc 0, 0, [LitPush Unit, Return], []) else None)
lemma method_append:
method (E, list_name) (append_name, [Class list_name]) = Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])
lemma method_makelist:
method (E, test_name) (makelist_name, []) = Some (test_name, PrimT Void, 3, 2, make_list_ins, [])
lemma method_default_ctor:
method (E, list_name) (init, []) =
Some (list_name, PrimT Void, 1, 0,
[Load 0, Invoke_special Object init [], Return], [])
lemma field_val:
field (E, list_name) val_name = Some (list_name, PrimT Integer)
lemma field_next:
field (E, list_name) next_name = Some (list_name, Class list_name)
lemma
fields (E, Object) = []
lemma
fields (E, Xcpt NullPointer) = []
lemma
fields (E, Xcpt ClassCast) = []
lemma
fields (E, Xcpt OutOfMemory) = []
lemma
fields (E, test_name) = []
lemmas
is_class G C == class G C ~= None
lemma pc_0:
[| x < n; x \<in> [0, n) ==> P x |] ==> P x
lemma pc_next:
[| x \<in> [n0, n); P n0; x \<in> [Suc n0, n) ==> P x |] ==> P x
lemma pc_end:
x \<in> [n, n) ==> P x
lemma wf_struct:
wf_prog (%G C mb. True) E
lemmas eff_simps:
eff i G pc et s == map (%pc'. (pc', norm_eff i G pc s)) (succs i pc) @ xcpt_eff i G pc s et
norm_eff i G pc == option_map (eff_bool i G pc)
xcpt_eff i G pc s et ==
map (%C. (the (match_exception_table G C pc et),
case s of None => None
| Some s' => Some (([Init (Class C)], snd (fst s')), snd s')))
(xcpt_names (i, G, pc, et))
eff_bool i G pc ==
%((ST, LT), z).
(eff' (i, G, pc, ST, LT),
if EX C p D. i = Invoke_special C init p & ST ! length p = PartInit D
then True else z)
subtype G T1 T2 == G |- T1 <= T2
lemma list_all'_rec:
list_all'_rec P n xs = (ALL p. p < length xs --> P (xs ! p) (p + n))
lemma list_all':
list_all' P xs = (ALL n. n < length xs --> P (xs ! n) n)
lemma list_all_ball:
list_all P xs = Ball (set xs) P
lemma
check_bounded ins et = (list_all' (%i pc. list_all (%pc'. pc' < length ins) (succs i pc)) ins & list_all (%e. fst (snd (snd e)) < length ins) et)
lemma init_tys_def2:
init_tys E =
{Init y |y. is_type E y} Un {UnInit c n |c n. True} Un {PartInit c |c. True}
lemma check_types_lemma:
[| b : list mxr (err (init_tys E)); a : list (length a) (init_tys E);
length a <= mxs |]
==> OK (Some ((a, b), x)) : states E mxs mxr
lemma Object_init:
wt_method E Object init [] (PrimT Void) (Suc 0) 0 [LitPush Unit, Return] [] \<phi>\<^sub>o
lemma
Ex Not
lemma
EX z. z
lemma default_ctor:
[| E |- C <=C1 Object; is_class E C |]
==> wt_method E C init [] (PrimT Void) (Suc 0) 0
[Load 0, Invoke_special Object init [], Return] [] \<phi>\<^sub>c C
lemma wt_append:
wt_method E list_name append_name [Class list_name] (PrimT Void) 3 0 append_ins [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a
lemma wt_makelist:
wt_method E test_name makelist_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m
lemma
is_class E C =
(C : {Cname list_nam, Cname test_nam, Xcpt NullPointer, Xcpt ClassCast,
Xcpt OutOfMemory, Object})
lemma wf_prog:
wt_jvm_prog E \<Phi>
lemma
E,\<Phi> |-JVM start_state E test_name makelist_name [ok]