Up to index of Isabelle/Bali5
theory Example = Eval + WellForm(* Title: isabelle/Bali/Example.thy
ID: $Id: Example.thy,v 1.39 2000/11/29 22:48:45 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]) ;
}
}
}
*)
Example = Eval + WellForm + (** cannot simply instantiate tnam **)
datatype tnam_ = HasFoo_ | Base_ | Ext_
datatype enam_ = arr_ | 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 \<equiv> []"
SXcpt_mdecls_def "SXcpt_mdecls \<equiv> []"
syntax
HasFoo, Base, Ext :: tname
arr, vee, z, 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_"
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)
))"
arr_viewed_from :: "tname \<Rightarrow> var"
"arr_viewed_from C \<equiv> {Base,True}StatRef (ClassT C)..arr"
constdefs
HasFooInt :: iface
"HasFooInt \<equiv> ([], [(foo_sig, foo_mhead)])"
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
ifaces :: idecl list
"ifaces \<equiv> [(HasFoo,HasFooInt)]"
clsses :: cdecl list (** name not 'classes' because of clash with thy token**)
"clsses \<equiv> [(Base,BaseCl),(Ext,ExtCl)]@standard_classes"
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)"
consts
a,b,c :: loc
syntax
"classes" :: cdecl list
tprg :: prog
obj_a, obj_b, obj_c :: obj
arr_N, arr_a :: (vn, val) table
globs1,globs2,
globs3,globs8 :: globs
locs3,locs4,locs8 :: locals
s0,s0',s9',
s1,s1',s2,s2',
s3,s3',s4,s4',
s6',s7',s8,s8' :: state
translations
"classes" == "clsses"
"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)"
end
theorem wf_fdecl_def2:
wf_fdecl G fd = is_type G (snd (snd fd))
theorem table_ifaces:
table_of ifaces = empty(HasFoo|->HasFooInt)
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_HasFoo:
table_of classes HasFoo = None [!]
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 ws_idecl_HasFoo:
ws_idecl tprg HasFoo []
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_idecl_all:
G = tprg ==> ALL (I, si, ib):set ifaces. ws_idecl G I si
theorem ws_cdecl_all:
G = tprg ==> ALL (C, sc, cb):set classes. ws_cdecl G C sc [!]
theorem ws_tprg:
ws_prog tprg [!]
theorem single_iface:
is_iface tprg I = (I = HasFoo)
theorem empty_subint1:
subint1 tprg = {}
theorem unique_ifaces:
unique ifaces
theorem unique_classes:
unique classes [!]
theorem SXcpt_subcls_Throwable:
tprg|-SXcpt xn<=:C SXcpt Throwable [!]
theorem Ext_subcls_Base:
tprg|-Ext<=:C Base [!]
theorem fields_tprg_Object:
fields tprg Object = [] [!]
theorem fields_tprg_Throwable:
fields tprg (SXcpt Throwable) = [] [!]
theorem fields_tprg_SXcpt:
fields tprg (SXcpt xn) = [] [!]
theorem fields_Base:
fields tprg Base =
[((arr, Base), True, PrimT Boolean.[]), ((vee, Base), False, Iface HasFoo)]
[!]
theorem fields_Ext:
fields tprg Ext = [((vee, Ext), False, PrimT Integer)] @ fields tprg Base [!]
theorem imethds_HasFoo:
imethds tprg HasFoo = o2s o empty(foo_sig|->(HasFoo, foo_mhead)) [!]
theorem cmethd_tprg_Object:
cmethd tprg Object = empty [!]
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_HasFoo:
wf_idecl tprg (HasFoo, HasFooInt) [!]
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_idecl_all:
p = tprg ==> Ball (set ifaces) (wf_idecl p) [!]
theorem wf_cdecl_all_standard_classes:
Ball (set standard_classes) (wf_cdecl tprg) [!]
theorem wf_cdecl_all:
p = tprg ==> Ball (set classes) (wf_cdecl p) [!]
theorem wf_tprg:
wf_prog tprg [!]
theorem appl_methds_Base_foo:
appl_methds tprg (ClassT Base) (foo, [NT]) =
{((ClassT Base, False, [z], Class Base), [Class Base])}
[!]
theorem max_spec_Base_foo:
max_spec tprg (ClassT Base) (foo, [NT]) =
{((ClassT Base, False, [z], Class Base), [Class Base])}
[!]
theorem wt_test:
(tprg, empty(Inl e|->Class Base))|-test [Class Base]:<> [!]
theorem alloc_one:
[| the (new_Addr h) = a; atleast_free h (Suc n) |] ==> new_Addr h = Some a & atleast_free (h(a|->obj)) n
theorem 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'
[!]