Up to index of Isabelle/Bali5
theory Example = Eval + WellForm:(* Title: isabelle/Bali/Example.thy
ID: $Id: Example.thy,v 1.40 2001/05/11 14:41:58 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
The following example Bali program includes:
* class and interface declarations with inheritance, hiding of fields,
overriding of methods (with refined result type), array type,
* method call (with dynamic binding), parameter access, return expressions,
* expression statements, sequential composition, literal values,
local assignment, local access, field assignment, type cast,
* exception generation and propagation, try & catch statement, throw statement
* instance creation and (default) static initialization
interface HasFoo {
public Base foo(Base z);
}
class Base implements HasFoo {
static boolean arr[] = new boolean[2];
HasFoo vee;
public Base foo(Base z) {
return z;
}
}
class Ext extends Base {
int vee;
public Ext foo(Base z) {
((Ext)z).vee = 1;
return null;
}
}
class Example {
public static void main(String args[]) throws Throwable {
Base e = new Ext();
try {e.foo(null); }
catch(NullPointerException z) {
while(Ext.arr[2]) ;
}
}
}
*)
theory Example = Eval + WellForm:
declare widen.null [intro]
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G fd = is_type G (snd (snd fd))"
apply (unfold wf_fdecl_def)
apply (simp (no_asm))
done
declare wf_fdecl_def2 [iff]
section "type and expression names"
(** unfortunately cannot simply instantiate tnam **)
datatype tnam_ = HasFoo_ | Base_ | Ext_
datatype enam_ = arr_ | vee_ | z_ | e_
consts
tnam_ :: "tnam_ \<Rightarrow> tnam"
enam_ :: "enam_ \<Rightarrow> ename"
axioms (** tnam_ and enam_ are intended to be isomorphic to tnam and ename **)
inj_tnam_ [simp]: "(tnam_ x = tnam_ y) = (x = y)"
inj_enam_ [simp]: "(enam_ x = enam_ y) = (x = y)"
surj_tnam_: "\<exists>m. n = tnam_ m"
surj_enam_: "\<exists>m. n = enam_ m"
syntax
HasFoo :: tname
Base :: tname
Ext :: tname
arr :: ename
vee :: ename
z :: ename
e :: ename
translations
"HasFoo" == "TName (tnam_ HasFoo_)"
"Base" == "TName (tnam_ Base_)"
"Ext" == "TName (tnam_ Ext_)"
"arr" == "enam_ arr_"
"vee" == "enam_ vee_"
"z" == "enam_ z_"
"e" == "enam_ e_"
section "classes and interfaces"
defs
Object_mdecls_def: "Object_mdecls \<equiv> []"
SXcpt_mdecls_def: "SXcpt_mdecls \<equiv> []"
consts
foo :: mname
constdefs
foo_sig :: sig
"foo_sig \<equiv> (foo,[Class Base])"
foo_mhead :: mhead
"foo_mhead \<equiv> (False,[z],Class Base)"
constdefs
Base_foo :: mdecl
"Base_foo \<equiv> (foo_sig, (foo_mhead,([],Skip,!!z)))"
Ext_foo :: mdecl
"Ext_foo \<equiv> (foo_sig, ((False,[z],Class Ext),
([],Expr({Ext,False}Cast (Class Ext) (!!z)..vee :=
Lit (Intg #1)),Lit Null)
))"
constdefs
arr_viewed_from :: "tname \<Rightarrow> var"
"arr_viewed_from C \<equiv> {Base,True}StatRef (ClassT C)..arr"
BaseCl :: class
"BaseCl \<equiv> (Object, [HasFoo],
[(arr, (True, PrimT Boolean.[])),
(vee, (False, Iface HasFoo ))],
[Base_foo],
Expr(arr_viewed_from Base := New (PrimT Boolean)[Lit (Intg #2)]))"
ExtCl :: class
"ExtCl \<equiv> (Base , [],
[(vee, (False, PrimT Integer ))],
[Ext_foo],
Skip)"
constdefs
HasFooInt :: iface
"HasFooInt \<equiv> ([], [(foo_sig, foo_mhead)])"
ifaces ::"idecl list"
"ifaces \<equiv> [(HasFoo,HasFooInt)]"
"classes" ::"cdecl list"
"classes \<equiv> [(Base,BaseCl),(Ext,ExtCl)]@standard_classes"
lemmas table_classes_defs =
classes_def standard_classes_def ObjectC_def SXcptC_def
lemma table_ifaces [simp]: "table_of ifaces = empty(HasFoo\<mapsto>HasFooInt)"
apply (unfold ifaces_def)
apply (simp (no_asm))
done
lemma table_classes_Object [simp]:
"table_of classes Object = Some (arbitrary, [], [], Object_mdecls, Skip)"
apply (unfold table_classes_defs)
apply (simp (no_asm))
done
lemma table_classes_SXcpt [simp]:
"table_of classes (SXcpt xn) = Some (if xn = Throwable then Object
else SXcpt Throwable, [], [], SXcpt_mdecls, Skip)"
apply (unfold table_classes_defs)
apply (induct_tac xn)
apply simp+
done
lemma table_classes_HasFoo [simp]: "table_of classes HasFoo = None"
apply (unfold table_classes_defs)
apply (simp (no_asm))
done
lemma table_classes_Base [simp]: "table_of classes Base = Some BaseCl"
apply (unfold table_classes_defs )
apply (simp (no_asm))
done
lemma table_classes_Ext [simp]: "table_of classes Ext = Some ExtCl"
apply (unfold table_classes_defs )
apply (simp (no_asm))
done
section "program"
syntax
tprg :: prog
translations
"tprg" == "(ifaces,classes)"
constdefs
test :: "(ty)list \<Rightarrow> stmt"
"test pTs \<equiv> e:==NewC Ext;;
Try Expr({ClassT Base,ClassT Base,IntVir}!!e..
foo({pTs}[Lit Null]))
Catch((SXcpt NullPointer) z)
(While(Acc (Acc (arr_viewed_from Ext).[Lit (Intg #2)])) Skip)"
section "well-structuredness"
lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
apply (auto dest!: tranclD subcls1D)
done
lemma not_Throwable_subcls_SXcpt [elim!]:
"(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
apply (auto dest!: tranclD subcls1D)
done
lemma not_SXcpt_n_subcls_SXcpt_n [elim!]:
"(SXcpt xn, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
apply (auto dest!: tranclD subcls1D)
apply (drule rtranclD)
apply auto
done
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def)
done
lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]:
"(TName tn, TName tn) \<in> (subcls1 tprg)^+ \<longrightarrow> R"
apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE])
apply (erule ssubst)
apply (rule tnam_.induct)
apply safe
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def)
apply (drule rtranclD)
apply auto
done
lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []"
apply (unfold ws_idecl_def)
apply (simp (no_asm))
done
lemma ws_cdecl_Object: "ws_cdecl tprg Object any"
apply (unfold ws_cdecl_def)
apply auto
done
lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object"
apply (unfold ws_cdecl_def)
apply auto
done
lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)"
apply (unfold ws_cdecl_def)
apply auto
done
lemma ws_cdecl_Base: "ws_cdecl tprg Base Object"
apply (unfold ws_cdecl_def)
apply auto
done
lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base"
apply (unfold ws_cdecl_def)
apply auto
done
lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
ws_cdecl_Base ws_cdecl_Ext
declare not_Object_subcls_any [rule del]
not_Throwable_subcls_SXcpt [rule del]
not_SXcpt_n_subcls_SXcpt_n [rule del]
not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del]
lemma ws_idecl_all: "G=tprg \<Longrightarrow> (\<forall>(I,(si,ib))\<in>set ifaces. ws_idecl G I si)"
apply (simp (no_asm) add: ifaces_def HasFooInt_def)
apply (auto intro!: ws_idecl_HasFoo)
done
lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,(sc,cb))\<in>set classes. ws_cdecl G C sc)"
apply (simp (no_asm) add: classes_def BaseCl_def ExtCl_def)
apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def
SXcptC_def)
done
lemma ws_tprg: "ws_prog tprg"
apply (unfold ws_prog_def)
apply (auto intro!: ws_idecl_all ws_cdecl_all)
done
section "misc program properties (independent of well-structuredness)"
lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
apply (unfold ifaces_def)
apply (simp (no_asm))
done
lemma empty_subint1 [simp]: "subint1 tprg = {}"
apply (unfold subint1_def ifaces_def HasFooInt_def)
apply auto
done
lemma unique_ifaces: "unique ifaces"
apply (unfold ifaces_def)
apply (simp (no_asm))
done
lemma unique_classes: "unique classes"
apply (unfold table_classes_defs )
apply simp
done
lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable"
apply (rule SXcpt_subcls_Throwable_lemma)
apply force
done
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<preceq>C Base"
apply (rule subcls_direct)
apply (simp (no_asm) add: ExtCl_def)
apply (simp (no_asm))
done
section "fields and method lookup"
lemma fields_tprg_Object [simp]: "fields tprg Object = []"
by (rule ws_tprg [THEN fields_emptyI], force+)
lemma fields_tprg_Throwable [simp]: "fields tprg (SXcpt Throwable) = []"
by (rule ws_tprg [THEN fields_emptyI], force+)
lemma fields_tprg_SXcpt [simp]: "fields tprg (SXcpt xn) = []"
apply (case_tac "xn = Throwable")
apply (simp (no_asm_simp))
by (rule ws_tprg [THEN fields_emptyI], force+)
lemmas fields_rec_ = fields_rec [OF _ ws_tprg]
lemma fields_Base [simp]:
"fields tprg Base = [((arr, Base), (True, PrimT Boolean.[])),
((vee, Base), (False, Iface HasFoo ))]"
apply (subst fields_rec_)
apply (auto simp add: BaseCl_def)
done
lemma fields_Ext [simp]:
"fields tprg Ext = [((vee, Ext ), (False, PrimT Integer))] @ fields tprg Base"
apply (rule trans)
apply (rule fields_rec_)
apply (auto simp add: ExtCl_def)
done
lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg]
lemmas cmethd_rec_ = cmethd_rec [OF _ ws_tprg]
lemma imethds_HasFoo [simp]:
"imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
apply (rule trans)
apply (rule imethds_rec_)
apply (auto simp add: HasFooInt_def)
done
lemma cmethd_tprg_Object [simp]: "cmethd tprg Object = empty"
apply (subst cmethd_rec_)
apply (auto simp add: Object_mdecls_def)
done
lemma cmethd_Base [simp]:
"cmethd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]"
apply (rule trans)
apply (rule cmethd_rec_)
apply (auto simp add: BaseCl_def)
done
lemma cmethd_Ext [simp]: "cmethd tprg Ext = cmethd tprg Base ++
table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]"
apply (rule trans)
apply (rule cmethd_rec_)
apply (auto simp add: ExtCl_def)
done
section "well-formedness"
lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
apply (unfold wf_idecl_def HasFooInt_def)
apply (auto intro!: wf_mheadI ws_idecl_HasFoo
simp add: foo_sig_def foo_mhead_def)
done
declare wt.Skip [rule del] wt.Init [rule del]
lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
lemmas Ext_foo_defs = Ext_foo_def foo_sig_def
ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
lemmas wtIs = wt_Call wt_StatRef wt_intros
lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
apply (unfold Base_foo_defs )
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs)
done
lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
apply (unfold Ext_foo_defs )
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs)
apply (rule wt.Cast)
prefer 2
apply simp
apply (rule_tac [2] narrow.subcls [THEN cast.narrow])
apply (unfold cfield_def)
apply (auto intro!: wtIs)
done
lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
apply (auto intro!: wf_Base_foo)
apply (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
apply (auto intro!: wtIs simp add: cfield_def)
done
lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
apply (unfold wf_cdecl_def ExtCl_def)
apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
apply (auto dest: map_of_SomeD
simp add: Base_foo_defs Ext_foo_def hiding_entails_def)
done
lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set ifaces) (wf_idecl p)"
apply (simp (no_asm) add: ifaces_def)
apply (simp (no_asm_simp))
apply (rule wf_HasFoo)
done
lemma wf_cdecl_all_standard_classes:
"Ball (set standard_classes) (wf_cdecl tprg)"
apply (unfold standard_classes_def Let_def
ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
done
lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set classes) (wf_cdecl p)"
apply (simp (no_asm) add: classes_def)
apply (simp (no_asm_simp))
apply (rule wf_BaseC [THEN conjI])
apply (rule wf_ExtC [THEN conjI])
apply (rule wf_cdecl_all_standard_classes)
done
theorem wf_tprg: "wf_prog tprg"
apply (unfold wf_prog_def Let_def)
apply (simp (no_asm) add: unique_ifaces unique_classes)
apply (rule conjI)
apply ((simp (no_asm) add: classes_def standard_classes_def))
apply (rule conjI)
apply (cut_tac xn_cases)
apply ((simp (no_asm_simp) add: classes_def standard_classes_def))
apply (auto intro!: wf_idecl_all wf_cdecl_all)
done
section "max_spec"
lemma appl_methds_Base_foo:
"appl_methds tprg (ClassT Base) (foo, [NT]) =
{((ClassT Base, (False,[z],Class Base)), [Class Base])}"
apply (unfold appl_methds_def)
apply (simp (no_asm))
apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
apply (auto simp add: cmheads_def Base_foo_defs)
done
lemma max_spec_Base_foo: "max_spec tprg (ClassT Base) (foo, [NT]) =
{((ClassT Base, (False,[z],Class Base)), [Class Base])}"
apply (unfold max_spec_def)
apply (simp (no_asm) add: appl_methds_Base_foo)
apply auto
done
section "well-typedness"
lemma wt_test: "(tprg, empty(EName e\<mapsto>Class Base))\<turnstile>test ?pTs\<Colon>\<surd>"
apply (unfold test_def arr_viewed_from_def)
(* ?pTs = [Class Base] *)
apply (rule wtIs (* ;; *))
apply (rule wtIs (* Expr *))
apply (rule wtIs (* Ass *))
apply (rule wtIs (* LVar *))
apply (simp)
apply (simp)
apply (simp)
apply (rule wtIs (* NewC *))
apply (simp)
apply (simp)
apply (rule wtIs (* Try *))
prefer 4
apply (simp)
defer
apply (rule wtIs (* Expr *))
apply (rule wtIs (* Call *))
apply (rule wtIs (* Acc *))
apply (rule wtIs (* LVar *))
apply (simp)
apply (simp)
apply (rule wtIs (* Cons *))
apply (rule wtIs (* Lit *))
apply (simp)
apply (rule wtIs (* Nil *))
apply (simp)
apply (rule max_spec_Base_foo)
apply (simp)
apply (simp)
apply (simp)
apply (rule wtIs (* While *))
apply (rule wtIs (* Acc *))
apply (rule wtIs (* AVar *))
apply (rule wtIs (* Acc *))
apply (rule wtIs (* FVar *))
apply (rule wtIs (* StatRef *))
apply (simp)
apply (simp add: cfield_def)
apply (rule wtIs (* LVar *))
apply (simp)
apply (rule wtIs (* Skip *))
done
section "execution"
lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>
new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
apply (frule atleast_free_SucD)
apply (drule atleast_free_Suc [THEN iffD1])
apply clarsimp
apply (frule new_Addr_SomeI)
apply force
done
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
Base_foo_defs [simp]
ML {* bind_thms ("eval_intros", map
(simplify (simpset() delsimps [thm "Skip_eq"]
addsimps [thm "lvar_def"]) o
rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
lemmas eval_Is = eval_Init eval_StatRef XcptIs eval_intros
consts
a :: loc
b :: loc
c :: loc
syntax
tprg :: prog
obj_a :: obj
obj_b :: obj
obj_c :: obj
arr_N :: "(vn, val) table"
arr_a :: "(vn, val) table"
globs1 :: globs
globs2 :: globs
globs3 :: globs
globs8 :: globs
locs3 :: locals
locs4 :: locals
locs8 :: locals
s0 :: state
s0' :: state
s9' :: state
s1 :: state
s1' :: state
s2 :: state
s2' :: state
s3 :: state
s3' :: state
s4 :: state
s4' :: state
s6' :: state
s7' :: state
s8 :: state
s8' :: state
translations
"tprg" == "(ifaces,classes)"
"obj_a" <= "(Arr (PrimT Boolean) #2, empty(Inr #0\<mapsto>Bool False)(Inr #1\<mapsto>Bool False))"
"obj_b" <= "(CInst Ext,(empty(Inl (vee, Base)\<mapsto>Null )
(Inl (vee, Ext )\<mapsto>Intg #0)))"
"obj_c" == "(CInst (SXcpt NullPointer),empty)"
"arr_N" == "empty(Inl (arr, Base)\<mapsto>Null)"
"arr_a" == "empty(Inl (arr, Base)\<mapsto>Addr a)"
"globs1" == "empty(Inr Ext \<mapsto>(arbitrary, empty))
(Inr Base \<mapsto>(arbitrary, arr_N))
(Inr Object\<mapsto>(arbitrary, empty))"
"globs2" == "empty(Inr Ext \<mapsto>(arbitrary, empty))
(Inr Object\<mapsto>(arbitrary, empty))
(Inl a\<mapsto>obj_a)
(Inr Base \<mapsto>(arbitrary, arr_a))"
"globs3" == "globs2(Inl b\<mapsto>obj_b)"
"globs8" == "globs3(Inl c\<mapsto>obj_c)"
"locs3" == "empty(Inl e\<mapsto>Addr b)"
"locs4" == "empty(Inl z\<mapsto>Null)(Inr()\<mapsto>Addr b)"
"locs8" == "locs3(Inl z\<mapsto>Addr c)"
"s0" == " st empty empty"
"s0'" == " Norm s0"
"s1" == " st globs1 empty"
"s1'" == " Norm s1"
"s2" == " st globs2 empty"
"s2'" == " Norm s2"
"s3" == " st globs3 locs3 "
"s3'" == " Norm s3"
"s4" == " st globs3 locs4"
"s4'" == " Norm s4"
"s6'" == "(Some (StdXcpt NullPointer), s4)"
"s7'" == "(Some (StdXcpt NullPointer), s3)"
"s8" == " st globs8 locs8"
"s8'" == " Norm s8"
"s9'" == "(Some (StdXcpt IndOutBound), s8)"
declare Pair_eq [simp del]
lemma exec_test:
"\<lbrakk>the (new_Addr (heap s1)) = a;
the (new_Addr (heap ?s2)) = b;
the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>
atleast_free (heap s0) 4 \<Longrightarrow>
tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'"
apply (unfold test_def arr_viewed_from_def)
(* ?s9' = s9' *)
apply (simp (no_asm_use))
apply (drule (1) alloc_one, clarsimp)
apply (rule eval_Is (* ;; *))
apply (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
apply (erule_tac [2] V = "atleast_free ?h 4" in thin_rl)
apply (rule eval_Is (* Expr *))
apply (rule eval_Is (* Ass *))
apply (rule eval_Is (* LVar *))
apply (rule eval_Is (* NewC *))
(* begin init Ext *)
apply (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
apply (erule_tac V = "atleast_free ?h 3" in thin_rl)
apply (erule_tac [2] V = "atleast_free ?h 4" in thin_rl)
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
apply (rule eval_Is (* Init Ext *))
apply (simp)
apply (rule conjI)
prefer 2 apply (rule conjI HOL.refl)+
apply (rule eval_Is (* Init Base *))
apply (simp add: arr_viewed_from_def)
apply (rule conjI)
apply (rule eval_Is (* Init Object *))
apply (simp)
apply (rule conjI, rule HOL.refl)+
apply (rule HOL.refl)
apply (simp)
apply (rule conjI, rule_tac [2] HOL.refl)
apply (rule eval_Is (* Expr *))
apply (rule eval_Is (* Ass *))
apply (rule eval_Is (* FVar *))
apply (rule init_done, simp)
apply (rule eval_Is (* StatRef *))
apply (simp)
apply (rule eval_Is (* NewA *))
apply (simp)
apply (rule eval_Is (* Lit *))
apply (simp)
apply (rule halloc.New)
apply (simp (no_asm_simp))
apply (drule atleast_free_weaken,rotate_tac -1,drule atleast_free_weaken)
apply (simp (no_asm_simp))
apply (simp add: upd_gobj_def)
(* end init Ext *)
apply (rule halloc.New)
apply (drule alloc_one)
prefer 2 apply fast
apply (simp (no_asm_simp))
apply (drule atleast_free_weaken)
apply force
apply (simp)
apply (drule alloc_one)
apply (simp (no_asm_simp))
apply clarsimp
apply (erule_tac V = "atleast_free ?h 3" in thin_rl)
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
apply (simp (no_asm_use))
apply (rule eval_Is (* Try *))
apply (rule eval_Is (* Expr *))
(* begin method call *)
apply (rule eval_Is (* Call *))
apply (rule eval_Is (* Acc *))
apply (rule eval_Is (* LVar *))
apply (rule eval_Is (* Cons *))
apply (rule eval_Is (* Lit *))
apply (rule eval_Is (* Nil *))
apply (simp)
apply (simp)
apply (rule eval_Is (* Methd *))
apply (simp add: body_def Let_def)
apply (rule eval_Is (* Body *))
apply (rule init_done, simp)
apply (rule eval_Is (* Expr *))
apply (rule eval_Is (* Ass *))
apply (rule eval_Is (* FVar *))
apply (rule init_done, simp)
apply (rule eval_Is (* Cast *))
apply (rule eval_Is (* Acc *))
apply (rule eval_Is (* LVar *))
apply (simp)
apply (simp split del: split_if)
apply (rule eval_Is (* XcptE *))
apply (simp)
apply (rule HOL.refl [THEN conjI])+
apply (rule eval_Is (* XcptE *))
apply (simp)
(* end method call *)
apply (rule sxalloc.intros)
apply (rule halloc.New)
apply (erule alloc_one [THEN conjunct1])
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
apply (drule alloc_one [THEN conjunct1])
apply (simp (no_asm_simp))
apply (erule_tac V = "atleast_free ?h 2" in thin_rl)
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
apply simp
apply (rule eval_Is (* While *))
apply (rule eval_Is (* Acc *))
apply (rule eval_Is (* AVar *))
apply (rule eval_Is (* Acc *))
apply (rule eval_Is (* FVar *))
apply (rule init_done, simp)
apply (rule eval_Is (* StatRef *))
apply (simp)
apply (rule eval_Is (* Lit *))
apply (simp (no_asm_simp))
apply (simp add: in_bounds_def)
apply (tactic{* fast_tac (claset_of(theory "Main") addIs (thms "eval_Is")) 1 *})
done
declare Pair_eq [simp]
end
lemma wf_fdecl_def2:
wf_fdecl G fd = is_type G (snd (snd fd))
lemmas table_classes_defs:
classes == [(Base, BaseCl), (Ext, ExtCl)] @ standard_classes
standard_classes == [ObjectC, SXcptC Throwable, SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast, SXcptC NegArrSize, SXcptC IndOutBound, SXcptC ArrStore]
ObjectC == (Object, arbitrary, [], [], Object_mdecls, Skip)
SXcptC xn == (SXcpt xn, if xn = Throwable then Object else SXcpt Throwable, [], [], SXcpt_mdecls, Skip)
lemma table_ifaces:
table_of ifaces = empty(HasFoo|->HasFooInt)
lemma table_classes_Object:
table_of classes Object = Some (arbitrary, [], [], Object_mdecls, Skip) [!]
lemma table_classes_SXcpt:
table_of classes (SXcpt xn) =
Some (if xn = Throwable then Object else SXcpt Throwable, [], [], SXcpt_mdecls,
Skip)
[!]
lemma table_classes_HasFoo:
table_of classes HasFoo = None [!]
lemma table_classes_Base:
table_of classes Base = Some BaseCl [!]
lemma table_classes_Ext:
table_of classes Ext = Some ExtCl [!]
lemma not_Object_subcls_any:
(Object, C) : (subcls1 tprg)^+ ==> R
lemma not_Throwable_subcls_SXcpt:
(SXcpt Throwable, SXcpt xn) : (subcls1 tprg)^+ ==> R [!]
lemma not_SXcpt_n_subcls_SXcpt_n:
(SXcpt xn, SXcpt xn) : (subcls1 tprg)^+ ==> R [!]
lemma not_Base_subcls_Ext:
(Base, Ext) : (subcls1 tprg)^+ ==> R [!]
lemma not_TName_n_subcls_TName_n:
(TName tn, TName tn) : (subcls1 tprg)^+ ==> R [!]
lemma ws_idecl_HasFoo:
ws_idecl tprg HasFoo []
lemma ws_cdecl_Object:
ws_cdecl tprg Object any
lemma ws_cdecl_Throwable:
ws_cdecl tprg (SXcpt Throwable) Object [!]
lemma ws_cdecl_SXcpt:
ws_cdecl tprg (SXcpt xn) (SXcpt Throwable) [!]
lemma ws_cdecl_Base:
ws_cdecl tprg Base Object [!]
lemma ws_cdecl_Ext:
ws_cdecl tprg Ext Base [!]
lemmas ws_cdecls:
ws_cdecl tprg (SXcpt xn) (SXcpt Throwable) [!]
ws_cdecl tprg Object any
ws_cdecl tprg (SXcpt Throwable) Object [!]
ws_cdecl tprg Base Object [!]
ws_cdecl tprg Ext Base [!]
lemma ws_idecl_all:
G = tprg ==> ALL (I, si, ib):set ifaces. ws_idecl G I si
lemma ws_cdecl_all:
G = tprg ==> ALL (C, sc, cb):set classes. ws_cdecl G C sc [!]
lemma ws_tprg:
ws_prog tprg [!]
lemma single_iface:
is_iface tprg I = (I = HasFoo)
lemma empty_subint1:
subint1 tprg = {}
lemma unique_ifaces:
unique ifaces
lemma unique_classes:
unique classes [!]
lemma SXcpt_subcls_Throwable:
tprg|-SXcpt xn<=:C SXcpt Throwable [!]
lemma Ext_subcls_Base:
tprg|-Ext<=:C Base [!]
lemma fields_tprg_Object:
fields tprg Object = [] [!]
lemma fields_tprg_Throwable:
fields tprg (SXcpt Throwable) = [] [!]
lemma fields_tprg_SXcpt:
fields tprg (SXcpt xn) = [] [!]
lemmas fields_rec_:
class tprg C = Some (sc, si, fs, ms, ini)
==> fields tprg C =
map (split (%fn. Pair (fn, C))) fs @
(if C = Object then [] else fields tprg sc)
[!]
lemma fields_Base:
fields tprg Base =
[((arr, Base), True, PrimT Boolean.[]), ((vee, Base), False, Iface HasFoo)]
[!]
lemma fields_Ext:
fields tprg Ext = [((vee, Ext), False, PrimT Integer)] @ fields tprg Base [!]
lemmas imethds_rec_:
iface tprg I = Some (is, ms)
==> imethds tprg I =
Un_tables (imethds tprg ` set is) \<oplus>\<oplus>
(o2s o table_of (map (%(s, mh). (s, I, mh)) ms))
[!]
lemmas cmethd_rec_:
class tprg C = Some (sc, si, fs, ms, ini)
==> cmethd tprg C =
(if C = Object then empty else cmethd tprg sc) ++
table_of (map (%(s, m). (s, C, m)) ms)
[!]
lemma imethds_HasFoo:
imethds tprg HasFoo = o2s o empty(foo_sig|->(HasFoo, foo_mhead)) [!]
lemma cmethd_tprg_Object:
cmethd tprg Object = empty [!]
lemma cmethd_Base:
cmethd tprg Base = table_of [(%(s, m). (s, Base, m)) Base_foo] [!]
lemma cmethd_Ext:
cmethd tprg Ext = cmethd tprg Base ++ table_of [(%(s, m). (s, Ext, m)) Ext_foo]
[!]
lemma wf_HasFoo:
wf_idecl tprg (HasFoo, HasFooInt) [!]
lemmas Base_foo_defs:
Base_foo == (foo_sig, foo_mhead, [], Skip, !! z)
foo_sig == (foo, [Class Base])
foo_mhead == (False, [z], Class Base)
lemmas Ext_foo_defs:
Ext_foo ==
(foo_sig, (False, [z], Class Ext), [],
Expr ({Ext,False}Cast (Class Ext) (!! z)..vee:=Lit (Intg #1)), Lit Null)
foo_sig == (foo, [Class Base])
theorems wt_intros:
E,dt|=Skip:<> [!]
E,dt|=e:-T ==> E,dt|=Expr e:<> [!]
[| E,dt|=c1:<>; E,dt|=c2:<> |] ==> E,dt|=c1;; c2:<> [!]
[| E,dt|=e:-PrimT Boolean; E,dt|=c1:<>; E,dt|=c2:<> |]
==> E,dt|=If(e) c1 Else c2:<>
[!]
[| E,dt|=e:-PrimT Boolean; E,dt|=c:<> |] ==> E,dt|=While(e) c:<> [!]
[| E,dt|=e:-Class tn; fst E|-tn<=:C SXcpt Throwable |] ==> E,dt|=Throw e:<> [!]
[| E,dt|=c1:<>; fst E|-tn<=:C SXcpt Throwable; snd E (Inl vn) = None;
(fst E, snd E(Inl vn|->Class tn)),dt|=c2:<> |]
==> E,dt|=Try c1 Catch(tn vn) c2:<>
[!]
[| E,dt|=c1:<>; E,dt|=c2:<> |] ==> E,dt|=c1 Finally c2:<> [!]
is_class (fst E) C ==> E,dt|=init C:<> [!]
is_class (fst E) C ==> E,dt|=NewC C:-Class C [!]
[| is_type (fst E) T; E,dt|=i:-PrimT Integer |] ==> E,dt|=New T[i]:-T.[] [!]
[| E,dt|=e:-T; is_type (fst E) T'; fst E|-T<=:? T' |] ==> E,dt|=Cast T' e:-T'
[!]
[| E,dt|=e:-RefT T; fst E|-RefT T<=:? RefT T' |]
==> E,dt|=e InstOf T':-PrimT Boolean
[!]
typeof dt x = Some T ==> E,dt|=Lit x:-T [!]
[| snd E (Inr ()) = Some (Class C); C ~= Object;
class (fst E) C = Some (D, rest) |]
==> E,dt|=Super:-Class D
[!]
E,dt|=va:=T ==> E,dt|=Acc va:-T [!]
[| E,dt|=va:=T; va ~= LVar (Inr ()); E,dt|=v:-T'; fst E|-T'<=:T |]
==> E,dt|=va:=v:-T'
[!]
[| E,dt|=e0:-PrimT Boolean; E,dt|=e1:-T1; E,dt|=e2:-T2;
fst E|-T1<=:T2 & T = T2 | fst E|-T2<=:T1 & T = T1 |]
==> E,dt|=e0 ? e1 : e2:-T
[!]
[| E,dt|=e:-RefT t; E,dt|=ps:#pTs;
max_spec (fst E) t (mn, pTs) = {((md, m, pns, rT), pTs')} |]
==> E,dt|={t,md,invmode m e}e..mn( {pTs'}ps):-rT
[!]
[| is_class (fst E) C; cmethd (fst E) C sig = Some (md, mh, lvars, blk, res);
E,dt|=Body md blk res:-T |]
==> E,dt|=Methd C sig:-T
[!]
[| is_class (fst E) D; E,dt|=blk:<>; E,dt|=res:-T |] ==> E,dt|=Body D blk res:-T
[!]
[| snd E vn = Some T; is_type (fst E) T |] ==> E,dt|=LVar vn:=T [!]
[| E,dt|=e:-Class C; cfield (fst E) C fn = Some (fd, m, fT) |]
==> E,dt|={fd,m}e..fn:=fT
[!]
[| E,dt|=e:-T.[]; E,dt|=i:-PrimT Integer |] ==> E,dt|=e.[i]:=T [!]
E,dt|=[]:#[] [!]
[| E,dt|=e:-T; E,dt|=es:#Ts |] ==> E,dt|=e # es:#T # Ts [!]
lemmas wtIs:
[| E,dt|=e:-RefT t; E,dt|=ps:#pTs;
max_spec (fst E) t (mn, pTs) = {((md, m, pns, rT), pTs')};
mode = invmode m e |]
==> E,dt|={t,md,mode}e..mn( {pTs'}ps):-rT
[!]
isrtype (fst E) rt ==> E|-StatRef rt:-RefT rt [!]
E,dt|=Skip:<> [!]
E,dt|=e:-T ==> E,dt|=Expr e:<> [!]
[| E,dt|=c1:<>; E,dt|=c2:<> |] ==> E,dt|=c1;; c2:<> [!]
[| E,dt|=e:-PrimT Boolean; E,dt|=c1:<>; E,dt|=c2:<> |]
==> E,dt|=If(e) c1 Else c2:<>
[!]
[| E,dt|=e:-PrimT Boolean; E,dt|=c:<> |] ==> E,dt|=While(e) c:<> [!]
[| E,dt|=e:-Class tn; fst E|-tn<=:C SXcpt Throwable |] ==> E,dt|=Throw e:<> [!]
[| E,dt|=c1:<>; fst E|-tn<=:C SXcpt Throwable; snd E (Inl vn) = None;
(fst E, snd E(Inl vn|->Class tn)),dt|=c2:<> |]
==> E,dt|=Try c1 Catch(tn vn) c2:<>
[!]
[| E,dt|=c1:<>; E,dt|=c2:<> |] ==> E,dt|=c1 Finally c2:<> [!]
is_class (fst E) C ==> E,dt|=init C:<> [!]
is_class (fst E) C ==> E,dt|=NewC C:-Class C [!]
[| is_type (fst E) T; E,dt|=i:-PrimT Integer |] ==> E,dt|=New T[i]:-T.[] [!]
[| E,dt|=e:-T; is_type (fst E) T'; fst E|-T<=:? T' |] ==> E,dt|=Cast T' e:-T'
[!]
[| E,dt|=e:-RefT T; fst E|-RefT T<=:? RefT T' |]
==> E,dt|=e InstOf T':-PrimT Boolean
[!]
typeof dt x = Some T ==> E,dt|=Lit x:-T [!]
[| snd E (Inr ()) = Some (Class C); C ~= Object;
class (fst E) C = Some (D, rest) |]
==> E,dt|=Super:-Class D
[!]
E,dt|=va:=T ==> E,dt|=Acc va:-T [!]
[| E,dt|=va:=T; va ~= LVar (Inr ()); E,dt|=v:-T'; fst E|-T'<=:T |]
==> E,dt|=va:=v:-T'
[!]
[| E,dt|=e0:-PrimT Boolean; E,dt|=e1:-T1; E,dt|=e2:-T2;
fst E|-T1<=:T2 & T = T2 | fst E|-T2<=:T1 & T = T1 |]
==> E,dt|=e0 ? e1 : e2:-T
[!]
[| E,dt|=e:-RefT t; E,dt|=ps:#pTs;
max_spec (fst E) t (mn, pTs) = {((md, m, pns, rT), pTs')} |]
==> E,dt|={t,md,invmode m e}e..mn( {pTs'}ps):-rT
[!]
[| is_class (fst E) C; cmethd (fst E) C sig = Some (md, mh, lvars, blk, res);
E,dt|=Body md blk res:-T |]
==> E,dt|=Methd C sig:-T
[!]
[| is_class (fst E) D; E,dt|=blk:<>; E,dt|=res:-T |] ==> E,dt|=Body D blk res:-T
[!]
[| snd E vn = Some T; is_type (fst E) T |] ==> E,dt|=LVar vn:=T [!]
[| E,dt|=e:-Class C; cfield (fst E) C fn = Some (fd, m, fT) |]
==> E,dt|={fd,m}e..fn:=fT
[!]
[| E,dt|=e:-T.[]; E,dt|=i:-PrimT Integer |] ==> E,dt|=e.[i]:=T [!]
E,dt|=[]:#[] [!]
[| E,dt|=e:-T; E,dt|=es:#Ts |] ==> E,dt|=e # es:#T # Ts [!]
lemma wf_Base_foo:
wf_mdecl tprg Base Base_foo [!]
lemma wf_Ext_foo:
wf_mdecl tprg Ext Ext_foo [!]
lemma wf_BaseC:
wf_cdecl tprg (Base, BaseCl) [!]
lemma wf_ExtC:
wf_cdecl tprg (Ext, ExtCl) [!]
lemma wf_idecl_all:
p = tprg ==> Ball (set ifaces) (wf_idecl p) [!]
lemma wf_cdecl_all_standard_classes:
Ball (set standard_classes) (wf_cdecl tprg) [!]
lemma wf_cdecl_all:
p = tprg ==> Ball (set classes) (wf_cdecl p) [!]
theorem wf_tprg:
wf_prog tprg [!]
lemma appl_methds_Base_foo:
appl_methds tprg (ClassT Base) (foo, [NT]) =
{((ClassT Base, False, [z], Class Base), [Class Base])}
[!]
lemma max_spec_Base_foo:
max_spec tprg (ClassT Base) (foo, [NT]) =
{((ClassT Base, False, [z], Class Base), [Class Base])}
[!]
lemma wt_test:
(tprg, empty(Inl e|->Class Base))|-test [Class Base]:<> [!]
lemma alloc_one:
[| the (new_Addr h) = a; atleast_free h (Suc n) |] ==> new_Addr h = Some a & atleast_free (h(a|->obj)) n
theorems eval_intros:
G|-(Some xc, s) -t>-> (arbitrary3 t, Some xc, s) [!]
G|-Norm s -Skip-> Norm s [!]
G|-Norm s0 -e->v-> s1 ==> G|-Norm s0 -Expr e-> s1 [!]
[| G|-Norm s0 -c1-> s1; G|-s1 -c2-> s2 |] ==> G|-Norm s0 -c1;; c2-> s2 [!]
[| G|-Norm s0 -e->b-> s1; G|-s1 -(if the_Bool b then c1 else c2)-> s2 |]
==> G|-Norm s0 -If(e) c1 Else c2-> s2
[!]
[| G|-Norm s0 -e->b-> s1;
if the_Bool b then G|-s1 -c-> s2 & G|-s2 -While(e) c-> s3 else s3 = s1 |]
==> G|-Norm s0 -While(e) c-> s3
[!]
G|-Norm s0 -e->a'-> s1 ==> G|-Norm s0 -Throw e-> xupd (throw a') s1 [!]
[| G|-Norm s0 -c1-> s1; G|-s1 -sxalloc-> s2;
if G,s2\<turnstile>catch C then G|-new_xcpt_var vn s2 -c2-> s3
else s3 = s2 |]
==> G|-Norm s0 -Try c1 Catch(C vn) c2-> s3
[!]
[| G|-Norm s0 -c1-> (x1, s1); G|-Norm s1 -c2-> s2 |]
==> G|-Norm s0 -c1 Finally c2-> xupd (xcpt_if (EX y. x1 = Some y) x1) s2
[!]
[| the (class G C) = (sc, si, fs, ms, ini);
if inited C (globs s0) then s3 = Norm s0
else G|-Norm ((init_class_obj G C)
s0) -(if C = Object then Skip else init sc)-> s1 &
G|-(set_lvars empty) s1 -ini-> s2 &
s3 = (set_lvars (locals (snd s1))) s2 |]
==> G|-Norm s0 -init C-> s3
[!]
[| G|-Norm s0 -init C-> s1; G|-s1 -halloc CInst C>a-> s2 |]
==> G|-Norm s0 -NewC C->Addr a-> s2
[!]
[| G|-Norm s0 -init_comp_ty T-> s1; G|-s1 -e->i'-> s2;
G|-xupd (check_neg i') s2 -halloc Arr T (the_Intg i')>a-> s3 |]
==> G|-Norm s0 -New T[e]->Addr a-> s3
[!]
[| G|-Norm s0 -e->v-> s1;
s2 = xupd (raise_if (¬ G,snd s1\<turnstile>v fits T) ClassCast) s1 |]
==> G|-Norm s0 -Cast T e->v-> s2
[!]
[| G|-Norm s0 -e->v-> s1; b = (v ~= Null & G,snd s1\<turnstile>v fits RefT T) |]
==> G|-Norm s0 -e InstOf T->Bool b-> s1
[!]
G|-Norm s -Lit v->v-> Norm s [!]
G|-Norm s -Super->the (locals s (Inr ()))-> Norm s [!]
G|-Norm s0 -va=>(v, f)-> s1 ==> G|-Norm s0 -Acc va->v-> s1 [!]
[| G|-Norm s0 -va=>(w, f)-> s1; G|-s1 -e->v-> s2 |]
==> G|-Norm s0 -va:=e->v-> (%(x, s).
(%(x', s'). (x', if x' = None then s' else s))
((if x = None then f v else id) (x, s)))
s2
[!]
[| G|-Norm s0 -e0->b-> s1; G|-s1 -(if the_Bool b then e1 else e2)->v-> s2 |]
==> G|-Norm s0 -e0 ? e1 : e2->v-> s2
[!]
[| G|-Norm s0 -e->a'-> s1; G|-s1 -args#>vs-> s2; C = target mode (snd s2) a' cT;
G|-init_lvars G C (mn, pTs) mode a' vs s2 -Methd C (mn, pTs)->v-> s3 |]
==> G|-Norm s0 -{t,cT,mode}e..mn( {pTs}args)->v-> (set_lvars (locals (snd s2)))
s3
[!]
G|-Norm s0 -body G C sig->v-> s1 ==> G|-Norm s0 -Methd C sig->v-> s1 [!]
[| G|-Norm s0 -init D-> s1; G|-s1 -c-> s2; G|-s2 -e->v-> s3 |]
==> G|-Norm s0 -Body D c e->v-> s3
[!]
G|-Norm s -LVar vn=>(the (locals s vn), %v. supd lupd(vn\<mapsto>v))-> Norm s
[!]
[| G|-Norm s0 -init C-> s1; G|-s1 -e->a-> s2; (v, s2') = fvar C stat fn a s2 |]
==> G|-Norm s0 -{C,stat}e..fn=>v-> s2'
[!]
[| G|-Norm s0 -e1->a-> s1; G|-s1 -e2->i-> s2; (v, s2') = avar G i a s2 |]
==> G|-Norm s0 -e1.[e2]=>v-> s2'
[!]
G|-Norm s0 -[]#>[]-> Norm s0 [!]
[| G|-Norm s0 -e->v-> s1; G|-s1 -es#>vs-> s2 |]
==> G|-Norm s0 -e # es#>v # vs-> s2
[!]
lemmas eval_Is:
if inited C (globs s0) then s3 = Norm s0
else G|-Norm ((init_class_obj G C)
s0) -(if C = Object then Skip
else init (fst (the (class G C))))-> s1 &
G|-(set_lvars empty) s1 -snd (snd (snd (snd (the (class G C)))))-> s2 &
s3 = (set_lvars (locals (snd s1))) s2
==> G|-Norm s0 -init C-> s3
[!]
G|-s -StatRef rt->(if fst s = None then Null else arbitrary)-> s [!]
G|-(Some xc, s) -x->arbitrary-> (Some xc, s) [!]
G|-(Some xc, s) -x=>arbitrary-> (Some xc, s) [!]
G|-(Some xc, s) -x#>arbitrary-> (Some xc, s) [!]
G|-(Some xc, s) -x-> (Some xc, s) [!]
G|-(Some xc, s) -t>-> (arbitrary3 t, Some xc, s) [!]
G|-Norm s -Skip-> Norm s [!]
G|-Norm s0 -e->v-> s1 ==> G|-Norm s0 -Expr e-> s1 [!]
[| G|-Norm s0 -c1-> s1; G|-s1 -c2-> s2 |] ==> G|-Norm s0 -c1;; c2-> s2 [!]
[| G|-Norm s0 -e->b-> s1; G|-s1 -(if the_Bool b then c1 else c2)-> s2 |]
==> G|-Norm s0 -If(e) c1 Else c2-> s2
[!]
[| G|-Norm s0 -e->b-> s1;
if the_Bool b then G|-s1 -c-> s2 & G|-s2 -While(e) c-> s3 else s3 = s1 |]
==> G|-Norm s0 -While(e) c-> s3
[!]
G|-Norm s0 -e->a'-> s1 ==> G|-Norm s0 -Throw e-> xupd (throw a') s1 [!]
[| G|-Norm s0 -c1-> s1; G|-s1 -sxalloc-> s2;
if G,s2\<turnstile>catch C then G|-new_xcpt_var vn s2 -c2-> s3
else s3 = s2 |]
==> G|-Norm s0 -Try c1 Catch(C vn) c2-> s3
[!]
[| G|-Norm s0 -c1-> (x1, s1); G|-Norm s1 -c2-> s2 |]
==> G|-Norm s0 -c1 Finally c2-> xupd (xcpt_if (EX y. x1 = Some y) x1) s2
[!]
[| the (class G C) = (sc, si, fs, ms, ini);
if inited C (globs s0) then s3 = Norm s0
else G|-Norm ((init_class_obj G C)
s0) -(if C = Object then Skip else init sc)-> s1 &
G|-(set_lvars empty) s1 -ini-> s2 &
s3 = (set_lvars (locals (snd s1))) s2 |]
==> G|-Norm s0 -init C-> s3
[!]
[| G|-Norm s0 -init C-> s1; G|-s1 -halloc CInst C>a-> s2 |]
==> G|-Norm s0 -NewC C->Addr a-> s2
[!]
[| G|-Norm s0 -init_comp_ty T-> s1; G|-s1 -e->i'-> s2;
G|-xupd (check_neg i') s2 -halloc Arr T (the_Intg i')>a-> s3 |]
==> G|-Norm s0 -New T[e]->Addr a-> s3
[!]
[| G|-Norm s0 -e->v-> s1;
s2 = xupd (raise_if (¬ G,snd s1\<turnstile>v fits T) ClassCast) s1 |]
==> G|-Norm s0 -Cast T e->v-> s2
[!]
[| G|-Norm s0 -e->v-> s1; b = (v ~= Null & G,snd s1\<turnstile>v fits RefT T) |]
==> G|-Norm s0 -e InstOf T->Bool b-> s1
[!]
G|-Norm s -Lit v->v-> Norm s [!]
G|-Norm s -Super->the (locals s (Inr ()))-> Norm s [!]
G|-Norm s0 -va=>(v, f)-> s1 ==> G|-Norm s0 -Acc va->v-> s1 [!]
[| G|-Norm s0 -va=>(w, f)-> s1; G|-s1 -e->v-> s2 |]
==> G|-Norm s0 -va:=e->v-> (%(x, s).
(%(x', s'). (x', if x' = None then s' else s))
((if x = None then f v else id) (x, s)))
s2
[!]
[| G|-Norm s0 -e0->b-> s1; G|-s1 -(if the_Bool b then e1 else e2)->v-> s2 |]
==> G|-Norm s0 -e0 ? e1 : e2->v-> s2
[!]
[| G|-Norm s0 -e->a'-> s1; G|-s1 -args#>vs-> s2; C = target mode (snd s2) a' cT;
G|-init_lvars G C (mn, pTs) mode a' vs s2 -Methd C (mn, pTs)->v-> s3 |]
==> G|-Norm s0 -{t,cT,mode}e..mn( {pTs}args)->v-> (set_lvars (locals (snd s2)))
s3
[!]
G|-Norm s0 -body G C sig->v-> s1 ==> G|-Norm s0 -Methd C sig->v-> s1 [!]
[| G|-Norm s0 -init D-> s1; G|-s1 -c-> s2; G|-s2 -e->v-> s3 |]
==> G|-Norm s0 -Body D c e->v-> s3
[!]
G|-Norm s -LVar vn=>(the (locals s vn), %v. supd lupd(vn\<mapsto>v))-> Norm s
[!]
[| G|-Norm s0 -init C-> s1; G|-s1 -e->a-> s2; (v, s2') = fvar C stat fn a s2 |]
==> G|-Norm s0 -{C,stat}e..fn=>v-> s2'
[!]
[| G|-Norm s0 -e1->a-> s1; G|-s1 -e2->i-> s2; (v, s2') = avar G i a s2 |]
==> G|-Norm s0 -e1.[e2]=>v-> s2'
[!]
G|-Norm s0 -[]#>[]-> Norm s0 [!]
[| G|-Norm s0 -e->v-> s1; G|-s1 -es#>vs-> s2 |]
==> G|-Norm s0 -e # es#>v # vs-> s2
[!]
lemma exec_test:
[| the (new_Addr (heap s1)) = a; the (new_Addr (heap s2)) = b;
the (new_Addr (heap s3)) = c; atleast_free (heap s0) 4 |]
==> tprg|-s0' -test [Class Base]-> s9'
[!]