Up to index of Isabelle/Bali4
theory Example = Eval + WellForm(* Title: isabelle/Bali/Example.thy
ID: $Id: Example.thy,v 1.30 2000/08/07 21:07:48 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
The following example Bali program includes:
class declarations with inheritance, hiding of fields, and overriding of
methods (with refined result type),
instance creation, local assignment, sequential composition,
try & catch, method call with dynamic binding, literal values,
expression statement, local access, type cast, field assignment (in part), skip
class Base {
boolean vee;
Base foo(Base z) {return z;}
}
class Ext extends Base{
int vee;
Ext foo(Base z) {((Ext)z).vee=1; return null;}
}
class Example {
public static void main (String args[]) {
Base e=new Ext();
try {e.foo(null); }
catch (NullPointerException z) {throw z;}
}
}
*)
Example = Eval + WellForm +
datatype tnam_ = Base_ | Ext_
datatype enam_ = vee_ | z_ | e_
consts
tnam_ :: "tnam_ \<Rightarrow> tnam"
enam_ :: "enam_ \<Rightarrow> ename"
rules (* tnam_ and enam_ are intended to be isomorphic to tnam and ename *)
inj_tnam_ "(tnam_ x = tnam_ y) = (x = y)"
inj_enam_ "(enam_ x = enam_ y) = (x = y)"
surj_tnam_ "\<exists>m. n = tnam_ m"
surj_enam_ "\<exists>m. n = enam_ m"
defs
Object_mdecls_def "Object_mdecls == []"
SXcpt_mdecls_def "SXcpt_mdecls == []"
syntax
Base, Ext :: tname
vee, z, e :: ename
translations
"Base" == "TName (tnam_ Base_)"
"Ext" == "TName (tnam_ Ext_)"
"vee" == "enam_ vee_"
"z" == "enam_ z_"
"e" == "enam_ e_"
consts
"classes" :: cdecl list
BaseCl, ExtCl :: class
Base_foo, Ext_foo :: mdecl
test :: stmt
foo :: mname
a,b :: loc
defs
Base_foo_def "Base_foo \<equiv> ((foo,[Class Base]),
(False,[z],Class Base),([],Skip,!!z))"
BaseCl_def "BaseCl \<equiv> (Object, [],
[(vee, (False, PrimT Boolean))],
[Base_foo],
Skip)"
Ext_foo_def "Ext_foo \<equiv> ((foo,[Class Base]),
(False,[z],Class Ext),
([],Expr({Ext,False}Cast (Class Ext) (!!z)..
vee:=Lit (Intg #1)),
Lit Null))"
ExtCl_def "ExtCl \<equiv> (Base , [],
[(vee, (False,PrimT Integer))],
[Ext_foo],
Skip)"
classes_def "classes \<equiv> [(Base,BaseCl),(Ext,ExtCl)]@standard_classes"
test_def "test \<equiv> Expr(e:==NewC Ext);;
\<spacespace> Try Expr({ClassT Base,ClassT Base,IntVir}!!e..
foo({[Class Base]}[Lit Null]))
\<spacespace> Catch((SXcpt NullPointer) z) (Throw (!!z))"
syntax
NP :: xname
tprg :: prog
obj1, obj2 :: obj
stats,globs1,globs2 :: globs
locs1, locs2 :: locals
s0',s0,s1,s2,s3,s4,s5,s6,s7:: state
translations
"NP" == "NullPointer"
"tprg" == "([],classes)"
"obj1" <= "(CInst Ext,(empty((vee, Base)\<mapsto>Bool False)
((vee, Ext )\<mapsto>Intg #0)) (+) empty)"
"obj2" == "(CInst(SXcpt NP),empty)"
"stats" == "empty(Inr Ext \<mapsto>(arbitrary, empty))
(Inr Base \<mapsto>(arbitrary, empty))
(Inr Object\<mapsto>(arbitrary, empty))"
"globs1" == "stats (Inl a\<mapsto>obj1)"
"globs2" == "globs1(Inl b\<mapsto>obj2)"
"locs1" == "empty(Inr()\<mapsto>Addr a)(Inl z\<mapsto>Null)"
"locs2" == "empty(Inl e\<mapsto>Addr a)(Inl z\<mapsto>Addr b)"
"s0'"== " Norm (st empty empty)"
"s0" == " Norm (st stats empty)"
"s1" == " Norm (st globs1 (empty(Inl e\<mapsto>Addr a)))"
"s2" == " Norm (st globs1 locs1)"
"s3" == "(Some (StdXcpt NP), st globs1 locs1)"
"s4" == "(Some (StdXcpt NP), st globs1 (empty(Inl e\<mapsto>Addr a)))"
"s5" == "(Some (XcptLoc b ), st globs2 (empty(Inl e\<mapsto>Addr a)))"
"s6" == " Norm (st globs2 locs2)"
"s7" == "(Some (XcptLoc b ), st globs2 locs2)"
end
theorem wf_fdecl_def2:
wf_fdecl G fd = is_type G (snd (snd fd))
theorem no_iface:
¬ is_iface tprg I
theorem no_subint1:
subint1 tprg = {}
theorem table_classes_Object:
table_of classes Object = Some (arbitrary, [], [], Object_mdecls, Skip)
theorem table_classes_SXcpt:
table_of classes (SXcpt xn) =
Some (if xn = Throwable then Object else SXcpt Throwable, [], [], SXcpt_mdecls,
Skip)
[!]
theorem table_classes_Base:
table_of classes Base = Some BaseCl
theorem table_classes_Ext:
table_of classes Ext = Some ExtCl
theorem not_Object_subcls_any:
(Object, C) : (subcls1 tprg)^+ ==> R
theorem not_Throwable_subcls_SXcpt:
(SXcpt Throwable, SXcpt xn) : (subcls1 tprg)^+ ==> R [!]
theorem not_SXcpt_n_subcls_SXcpt_n:
(SXcpt xn, SXcpt xn) : (subcls1 tprg)^+ ==> R [!]
theorem not_Base_subcls_Ext:
(Base, Ext) : (subcls1 tprg)^+ ==> R
theorem not_TName_n_subcls_TName_n:
(TName tn, TName tn) : (subcls1 tprg)^+ ==> R
theorem unique_classes:
unique classes [!]
theorem SXcpt_subcls_Throwable_:
tprg|-SXcpt xn<=:C SXcpt Throwable [!]
theorem Ext_subcls_Base:
tprg|-Ext<=:C Base
theorem ws_cdecl_Object:
ws_cdecl tprg Object any
theorem ws_cdecl_Throwable:
ws_cdecl tprg (SXcpt Throwable) Object
theorem ws_cdecl_SXcpt:
ws_cdecl tprg (SXcpt xn) (SXcpt Throwable) [!]
theorem ws_cdecl_Base:
ws_cdecl tprg Base Object
theorem ws_cdecl_Ext:
ws_cdecl tprg Ext Base
theorem ws_cdecl_all:
G = tprg ==> ALL (C, sc, cb):set classes. ws_cdecl G C sc [!]
theorem ws_tprg:
ws_prog tprg [!]
theorem fields_Object_:
fields tprg Object = [] [!]
theorem fields_Throwable_:
fields tprg (SXcpt Throwable) = [] [!]
theorem fields_SXcpt_:
fields tprg (SXcpt xn) = [] [!]
theorem fields_Base:
fields tprg Base = [((vee, Base), False, PrimT Boolean)] [!]
theorem fields_Ext:
fields tprg Ext = [((vee, Ext), False, PrimT Integer)] @ fields tprg Base [!]
theorem cmethd_Object_:
cmethd tprg Object = table_of [] [!]
theorem cmethd_Base:
cmethd tprg Base = table_of [(%(s, m). (s, Base, m)) Base_foo] [!]
theorem cmethd_Ext:
cmethd tprg Ext = cmethd tprg Base ++ table_of [(%(s, m). (s, Ext, m)) Ext_foo]
[!]
theorem wf_Base_foo:
wf_mdecl tprg Base Base_foo
theorem wf_Ext_foo:
wf_mdecl tprg Ext Ext_foo [!]
theorem wf_BaseC:
wf_cdecl tprg (Base, BaseCl) [!]
theorem wf_ExtC:
wf_cdecl tprg (Ext, ExtCl) [!]
theorem wf_tprg:
wf_prog tprg [!]
theorem appl_methds_Base_foo:
appl_methds tprg (ClassT Base) (foo, [NT]) =
{((ClassT Base, fst (snd Base_foo)), [Class Base])}
[!]
theorem max_spec_Base_foo:
max_spec tprg (ClassT Base) (foo, [NT]) =
{((ClassT Base, fst (snd Base_foo)), [Class Base])}
[!]
theorem wt_test:
(tprg, empty(Inl e
|->Class
Base))|-Expr (LVar (Inl e):=NewC Ext);; Try Expr
({ClassT
Base,ClassT
Base,IntVir}Acc (LVar (Inl
e))..foo( {[Class
Base]}[Lit Null])) Catch(SXcpt
NP z) Throw (Acc (LVar (Inl z))):<>
[!]
theorem exec_test:
[| new_Addr (heap (snd s0)) = Some a;
new_Addr (heap (st globs1 (empty(Inl e|->Addr a)))) = Some b; enough_mem |]
==> (s0', In1r test, In1 Unit, s7) : eval tprg
[!]