Up to index of Isabelle/HOL/arrays
theory BVExample = JVMListExample + BVSpecTypeSafe:(* Title: HOL/MicroJava/BV/BVExample.thy
ID: $Id: BVExample.html,v 1.1 2002/11/28 16:11:18 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_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,
Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize, Xcpt ArrayStore, Object}"
by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
text {* The subclass relation spelt out: *}
lemma subcls1:
"subcls1 E =
{(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object), (Xcpt ArrayStore, Object),
(Xcpt ArrayIndexOutOfBounds, Object), (Xcpt NegativeArraySize, Object)}"
(is "_ = ?set")
proof
show "?set \<subseteq> subcls1 E"
apply (simp add: subcls1_def2)
apply (unfold E_def system_defs class_def class_defs name_defs)
apply auto
done
show "subcls1 E \<subseteq> ?set"
apply rule
apply (erule subcls1.elims)
apply (drule class_SomeD)
apply (unfold E_def class_defs system_defs)
apply auto
done
qed
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 unique: "unique E"
by (unfold E_def class_defs system_defs name_defs) auto
lemma sys_classes_G: "sys_classes E"
apply (rule sys_classes.intro)
apply (clarsimp simp add: E_def)
apply (rule unique)
apply (rule wf_subcls1_E)
done
lemmas lookups [simp] = sys_lemmas [OF sys_classes_G]
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, 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 max_dim_def
have "unique E" by (rule unique)
moreover
have "wf_syscls E" by simp
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 ArrayIndexOutOfBoundsC"
by (auto elim: notin_rtrancl simp add: name_defs subcls1)
moreover
have "wf_cdecl ?mb E NegativeArraySizeC"
by (auto elim: notin_rtrancl simp add: name_defs subcls1)
moreover
have "wf_cdecl ?mb E ArrayStoreC"
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
declare
appInvoke [simp del]
appInvoke_special [simp del]
constdefs
phi_obj_ctor :: method_type ("\<phi>\<^sub>o")
"\<phi>\<^sub>o \<equiv> [{(([], [OK (Init (Class Object))]), True)},
{(([Init (PrimT Void)], [OK (Init (Class Object))]), True)}]"
lemma check_types_lemma [simp]:
"(\<forall>((a,b),x)\<in>A. b \<in> list mxr (err (init_tys E mpc)) \<and>
a \<in> list (length a) (init_tys E mpc) \<and>
length a \<le> mxs)
\<Longrightarrow>
OK A \<in> states E mxs mxr mpc"
apply (unfold states_def address_types_def)
apply simp
apply (rule subsetI)
apply clarify
apply (drule bspec, assumption)
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 init_tys_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> [{(([], [OK (PartInit C)]), False)},
{(([PartInit C], [OK (PartInit C)]), False)},
{(([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 init_tys_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 add: Object_ctor_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 (image (\<lambda>ST. ((map Init ST, map (OK \<circ> Init) [Class list_name, Class list_name]), False)))
[{ []},
{ [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]},
{ [PrimT Void]},
{ [Class list_name], [Class (Xcpt NullPointer)]},
{ []},
{ [Class list_name]},
{ [Class list_name, Class list_name]},
{ []},
{ [PrimT Void]}]"
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 init_tys_def)
apply clarify
apply (elim pc_end pc_next pc_0)
apply simp
apply simp
apply (clarsimp simp add: match_exception_entry_def)
apply simp
apply simp
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. {(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 init_tys_def list_class_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, Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize,
Xcpt ArrayStore, 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, NegativeArraySizeC, ArrayIndexOutOfBoundsC, ArrayStoreC]
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)
ArrayIndexOutOfBoundsC_decl ms == (Xcpt ArrayIndexOutOfBounds, Object, [], ms)
NegativeArraySizeC_decl ms == (Xcpt NegativeArraySize, Object, [], ms)
ArrayStoreC_decl ms == (Xcpt ArrayStore, Object, [], ms)
ObjectC == ObjectC_decl [Object_ctor]
NullPointerC == NullPointerC_decl [Default_ctor]
OutOfMemoryC == OutOfMemoryC_decl [Default_ctor]
ClassCastC == ClassCastC_decl [Default_ctor]
NegativeArraySizeC == NegativeArraySizeC_decl [Default_ctor]
ArrayStoreC == ArrayStoreC_decl [Default_ctor]
ArrayIndexOutOfBoundsC == ArrayIndexOutOfBoundsC_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_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,
Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize, Xcpt ArrayStore, Object}
lemma subcls1:
subcls1 E =
{(list_name, Object), (test_name, Object), (Xcpt NullPointer, Object),
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object),
(Xcpt ArrayStore, Object), (Xcpt ArrayIndexOutOfBounds, Object),
(Xcpt NegativeArraySize, 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 unique:
unique E
lemma sys_classes_G:
sys_classes E
lemmas lookups:
fields (E, Object) = []
class E Object = Some (arbitrary, [], [Object_ctor])
wf_syscls E
class E (Xcpt NullPointer) = Some (Object, [], [Default_ctor])
class E (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])
class E (Xcpt ClassCast) = Some (Object, [], [Default_ctor])
class E (Xcpt ArrayStore) = Some (Object, [], [Default_ctor])
class E (Xcpt NegativeArraySize) = Some (Object, [], [Default_ctor])
class E (Xcpt ArrayIndexOutOfBounds) = Some (Object, [], [Default_ctor])
fields (E, Xcpt NullPointer) = []
fields (E, Xcpt ClassCast) = []
fields (E, Xcpt OutOfMemory) = []
fields (E, Xcpt ArrayIndexOutOfBounds) = []
fields (E, Xcpt NegativeArraySize) = []
fields (E, Xcpt ArrayStore) = []
method (E, Object) sig = (if sig = (init, []) then Some (Object, snd Object_ctor) else None)
method (E, Xcpt NullPointer) sig = (if sig = (init, []) then Some (Xcpt NullPointer, snd Default_ctor) else None)
method (E, Xcpt ClassCast) sig = (if sig = (init, []) then Some (Xcpt ClassCast, snd Default_ctor) else None)
method (E, Xcpt OutOfMemory) sig = (if sig = (init, []) then Some (Xcpt OutOfMemory, snd Default_ctor) else None)
method (E, Xcpt ArrayIndexOutOfBounds) sig = (if sig = (init, []) then Some (Xcpt ArrayIndexOutOfBounds, snd Default_ctor) else None)
method (E, Xcpt NegativeArraySize) sig = (if sig = (init, []) then Some (Xcpt NegativeArraySize, snd Default_ctor) else None)
method (E, Xcpt ArrayStore) sig = (if sig = (init, []) then Some (Xcpt ArrayStore, snd Default_ctor) 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, 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 at == map (%pc'. (pc', norm_eff i G pc pc' at)) (succs i pc at) @ xcpt_eff i G pc at et
norm_eff i G pc pc' at ==
eff_bool i G pc `
(if EX idx. i = Ret idx then {s. s : at & pc' = theRA (theIdx i) s} else at)
xcpt_eff i G pc at et ==
map (%C. (the (match_exception_table G C pc et),
(%s. (([Init (Class C)], snd (fst s)), snd s)) ` at))
(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)
lemma check_types_lemma:
ALL ((a, b), x):A.
b : list mxr (err (init_tys E mpc)) &
a : list (length a) (init_tys E mpc) & length a <= mxs
==> OK A : states E mxs mxr mpc
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, Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize,
Xcpt ArrayStore, Object})
lemma wf_prog:
wt_jvm_prog E \<Phi>
lemma
E,\<Phi> |-JVM start_state E test_name makelist_name [ok]