Up to index of Isabelle/Bali4
theory WellForm = WellType(* Title: isabelle/Bali/WellForm.thy
ID: $Id: WellForm.thy,v 1.31 2000/09/11 19:29:05 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Well-formedness of Java programs
for static checks on expressions and statements, see WellType.thy
improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
* a method implementing or overwriting another method may have a result type
that widens to the result type of the other method (instead of identical type)
* if an interface inherits more than one method with the same signature, the
methods need not have identical return types
simplifications:
* Object and standard exceptions are assumed to be declared like normal classes
*)
WellForm = WellType +
consts
wf_fdecl :: "prog \<Rightarrow> \<spacespace> fdecl \<Rightarrow> bool"
wf_mhead :: "prog \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool"
wf_mdecl :: "prog \<Rightarrow> tname \<Rightarrow> mdecl \<Rightarrow> bool"
wf_idecl :: "prog \<Rightarrow> \<spacespace> idecl \<Rightarrow> bool"
wf_cdecl :: "prog \<Rightarrow> \<spacespace> cdecl \<Rightarrow> bool"
wf_prog :: "prog \<Rightarrow> \<spacespace> \<spacespace> bool"
defs
(* well-formed field declaration (common part for classes and interfaces),
cf. 8.3 and (9.3) *)
wf_fdecl_def "wf_fdecl G \<equiv> \<lambda>(fn,(m,ft)). is_type G ft"
(*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
(* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)
wf_mhead_def "wf_mhead G \<equiv> \<lambda>(mn,pTs) (m,pns,rT). length pTs = length pns \<and>
\<spacespace> ( \<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT \<and>
\<spacespace> nodups pns"
wf_mdecl_def "wf_mdecl G C \<equiv> \<lambda>((mn,pTs),(m,pns,rT),lvars,blk,res).
wf_mhead G \<spacespace> (mn,pTs) (m,pns,rT) \<and> unique lvars \<and>
(C=Object \<longrightarrow> ¬static m) \<and> (\<forall>(vn,T)\<in>set lvars. is_type G T) \<and>
(\<forall>pn\<in>set pns. table_of lvars pn = None) \<and>
(\<exists>T. (G,table_of lvars(pns[\<mapsto>]pTs) (+)¬static m ?\<mapsto>Class C)\<turnstile>
Body C blk res\<Colon>-T \<and> G\<turnstile>T\<preceq>rT)"
(* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
wf_idecl_def "wf_idecl G \<equiv> \<lambda>(I,(si,ms)). ws_idecl G I si \<and>
¬is_class G I \<and>
(\<forall>(sig,mh)\<in>set ms. wf_mhead G sig mh \<and> ¬static (fst mh)) \<and>
unique ms \<and>
(o2s \<circ> table_of ms hidings Un_tables((\<lambda>J.(imethds G J))``set si)
entails (\<lambda>mh (md,mh'). G\<turnstile>mrt mh\<preceq>mrt mh'))"
(* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)
wf_cdecl_def "wf_cdecl G \<equiv> \<lambda>(C,(sc,si,fs,ms,init)).
¬is_iface G C \<and>
(\<forall>I\<in>set si. is_iface G I \<and>
(\<forall>s. \<forall>(md', mh' ) \<in> imethds G I s.
(\<exists>(md ,(mh ,b)) \<in> cmethd G C s: G\<turnstile>mrt mh\<preceq>mrt mh' \<and>
¬static (fst mh)))) \<and>
(\<forall>f\<in>set fs. wf_fdecl G f) \<and> unique fs \<and>
(\<forall>m\<in>set ms. wf_mdecl G C m) \<and> unique ms \<and>
(G,empty)\<turnstile>init\<Colon>\<surd> \<and> ws_cdecl G C sc \<and>
(C \<noteq> Object \<longrightarrow> (table_of ms hiding cmethd G sc entails
(\<lambda>(mh,b) (md',(mh',b')). G\<turnstile>mrt mh\<preceq>mrt mh' \<and>
static (fst mh') = static (fst mh))))"
(* well-formed program, cf. 8.1, 9.1 *)
wf_prog_def "wf_prog G \<equiv> let is = fst G; cs = snd G in
ObjectC \<in> set cs \<and> (\<forall>xn. SXcptC xn \<in> set cs) \<and>
(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
(\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
end
theorem wf_fdecl_def2:
wf_fdecl G fd = is_type G (snd (snd fd))
theorem wf_mdeclI:
[| C = Object --> ¬ id m; length pTs = length pns; Ball (set pTs) (is_type G);
is_type G rT; nodups pns; unique lvars;
ALL pn:set pns. table_of lvars pn = None;
Ball (set lvars) (split (%vn. is_type G));
(G, table_of lvars(pns[|->]pTs
) (+)¬id m ?\<mapsto>Class C)|-Body C blk res:-T;
G|-T<=:rT |]
==> wf_mdecl G C ((mn, pTs), (m, pns, rT), lvars, blk, res)
theorem wf_mdeclD1:
wf_mdecl G C (sig, (m, pns, rT), lvars, blk, res)
==> wf_mhead G sig (m, pns, rT) &
unique lvars &
(ALL pn:set pns. table_of lvars pn = None) &
Ball (set lvars) (split (%vn. is_type G))
theorem wf_mdecl_bodyD:
wf_mdecl G C (sig, (m, pns, rT), lvars, blk, res)
==> EX T. (G, table_of lvars(pns[|->]snd sig
) (+)¬id m ?\<mapsto>Class C)|-Body C blk res:-T &
G|-T<=:rT
theorem static_Object_methodsE:
wf_mdecl G Object (sig, (True, pns, T), b) ==> R
theorem rT_is_type:
wf_mhead G sig (m, pns, rT) ==> is_type G rT
theorem wf_idecl_mhead:
[| wf_idecl G (I, is, ms); (s, mh) : set ms |] ==> wf_mhead G s mh & ¬ id (fst mh)
theorem wf_idecl_hidings:
wf_idecl G (I, is, ms)
==> %s. o2s (table_of ms
s) hidings Un_tables
(imethds G ``
set is) entails %mh (md, mh').
G|-snd (snd mh)<=:snd (snd mh')
theorem wf_idecl_supD:
[| wf_idecl G (I, is, ms); J : set is |] ==> is_iface G J & (J, I) ~: (subint1 G)^+
theorem wf_cdecl_unique:
wf_cdecl G (C, sc, si, fs, ms, ini) ==> unique fs & unique ms
theorem wf_cdecl_fdecl:
[| wf_cdecl G (C, sc, si, fs, ms, ini); f : set fs |] ==> wf_fdecl G f
theorem wf_cdecl_mdecl:
[| wf_cdecl G (C, sc, si, fs, ms, ini); m : set ms |] ==> wf_mdecl G C m
theorem wf_cdecl_impD:
[| wf_cdecl G (C, sc, si, fs, ms, ini); I : set si |]
==> is_iface G I &
(ALL s. ALL (md', mh'):imethds G I s.
? (md, mh, b):cmethd G C s:
G|-snd (snd mh)<=:snd (snd mh') & ¬ id (fst mh))
theorem wf_cdecl_supD:
[| wf_cdecl G (C, sc, si, fs, ms, ini); C ~= Object |]
==> is_class G sc &
(sc, C) ~: (subcls1 G)^+ &
(table_of
ms hiding cmethd G
sc entails %(mh, b) (md', mh', b').
G|-snd (snd mh)<=:snd (snd mh') &
fst mh' = fst mh)
theorem wf_cdecl_wt_init:
wf_cdecl G (C, sco, si, fs, ms, ini) ==> (G, empty)|-ini:<>
theorem wf_prog_idecl:
[| iface G I = Some i; wf_prog G |] ==> wf_idecl G (I, i)
theorem wf_prog_cdecl:
[| class G C = Some c; wf_prog G |] ==> wf_cdecl G (C, c)
theorem wf_ws_prog:
wf_prog G ==> ws_prog G
theorem class_Object:
wf_prog G ==> class G Object = Some (arbitrary, [], [], Object_mdecls, Skip)
theorem class_SXcpt:
wf_prog G
==> class G (SXcpt xn) =
Some (if xn = Throwable then Object else SXcpt Throwable, [], [],
SXcpt_mdecls, Skip)
theorem wf_ObjectC:
wf_cdecl G ObjectC = (¬ is_iface G Object & Ball (set Object_mdecls) (wf_mdecl G Object) & unique Object_mdecls)
theorem wf_SXcptC:
wf_cdecl G (SXcptC xn) =
(¬ is_iface G (SXcpt xn) &
Ball (set SXcpt_mdecls) (wf_mdecl G (SXcpt xn)) &
unique SXcpt_mdecls &
(let sc = if xn = Throwable then Object else SXcpt Throwable
in is_class G sc &
(sc, SXcpt xn) ~: (subcls1 G)^+ &
(table_of
SXcpt_mdecls hiding cmethd G
sc entails %(mh, b) (md', mh', b').
G|-snd (snd mh)<=:snd (snd mh') & fst mh' = fst mh)))
theorem Object_is_class:
wf_prog G ==> is_class G Object
theorem SXcpt_is_class:
wf_prog G ==> is_class G (SXcpt xn)
theorem cmethd_Object:
wf_prog G ==> cmethd G Object = table_of (map (%(s, m). (s, Object, m)) Object_mdecls)
theorem fields_Object:
wf_prog G ==> fields G Object = []
theorem cfield_Object:
wf_prog G ==> cfield G Object = empty
theorem fields_Throwable:
wf_prog G ==> fields G (SXcpt Throwable) = []
theorem fields_SXcpt:
wf_prog G ==> fields G (SXcpt xn) = []
theorem widen_trans:
[| G|-S<=:U; G|-U<=:T; wf_prog G |] ==> G|-S<=:T
theorem widen_trans2:
[| G|-U<=:T; G|-S<=:U; wf_prog G |] ==> G|-S<=:T
theorem Xcpt_subcls_Throwable:
wf_prog G ==> G|-SXcpt xn<=:C SXcpt Throwable
theorem unique_fields:
[| is_class G C; wf_prog G |] ==> unique (fields G C)
theorem fields_mono:
[| table_of (fields G C) fn = Some f; G|-D<=:C C; is_class G D; wf_prog G |] ==> table_of (fields G D) fn = Some f
theorem fields_is_type:
[| table_of (fields G C) m = Some (f, T); wf_prog G; is_class G C |] ==> is_type G T
theorem imethds_wf_mhead:
[| (md, mh) : imethds G I sig; wf_prog G; is_iface G I |] ==> wf_mhead G sig mh & ¬ id (fst mh)
theorem cmethd_wf_mdecl:
[| cmethd G C sig = Some (md, m); wf_prog G; class G C = Some y |] ==> G|-C<=:C md & is_class G md & wf_mdecl G md (sig, m)
theorem subcls_methd:
[| G|-C<=:C C'; is_class G C'; wf_prog G; cmethd G C' sig = Some x |]
==> (%(md, (m, pns, rT), mb).
? (md', (m', pns', rT'), mb'):cmethd G C sig:
id m' = id m & G|-rT'<=:rT)
x
theorem subint_widen_imethds:
[| G|-I<=:I J; wf_prog G; is_iface G J |]
==> ALL (md, m, pns, rT):imethds G J sig.
EX (md', m', pns', rT'):imethds G I sig. id m' = id m & G|-rT'<=:rT
theorem implmt1_methd:
[| G|-C~>1I; wf_prog G; (md, m, pn, rT) : imethds G I sig |] ==> ? (md', (m', pn', rT'), mb):cmethd G C sig: id m' = id m & G|-rT'<=:rT
theorem implmt_methd:
[| wf_prog G; G|-T''~>I; is_iface G I |]
==> ALL (md, m, pn, rT):imethds G I sig.
? (md', (m', pn', rT'), mb'):cmethd G T'' sig: id m' = id m & G|-rT'<=:rT
theorem mheadsD:
(md, mh) : mheads G t sig
==> (EX C D b.
t = ClassT C & md = ClassT D & cmethd G C sig = Some (D, mh, b)) |
(EX I. t = IfaceT I & (EX I'. (I', mh) : imethds G I sig) |
(EX D b. cmethd G Object sig = Some (D, mh, b))) |
(EX T D b. t = ArrayT T & cmethd G Object sig = Some (D, mh, b))
theorem class_mheadsD:
[| (md, m, pn, rT) : mheads G t sig; wf_prog G; class G C = Some y;
if EX T. t = ArrayT T then C = Object else G|-Class C<=:RefT t;
isrtype G t |]
==> ? (md', (m', pn', rT'), mb):cmethd G C sig: id m' = id m & G|-rT'<=:rT
theorem wt_is_type:
(G, L),dt|=v::T
==> wf_prog G -->
dt = empty_dt --> (is_type G (+) (%Ts. Ball (set Ts) (is_type G))) T
theorem ty_expr_is_type:
[| (G, L)|-e:-T; wf_prog G |] ==> is_type G T
theorem ty_var_is_type:
[| (G, L)|-v:=T; wf_prog G |] ==> is_type G T
theorem ty_exprs_is_type:
[| (G, L)|-es:#Ts; wf_prog G |] ==> Ball (set Ts) (is_type G)
theorem static_mheadsD:
[| (cT, m, pns, rT) : mheads G t sig; wf_prog G; (G, L)|-e:-RefT t;
m | e = Super |]
==> EX C D b.
t = ClassT C & cT = ClassT D & cmethd G C sig = Some (D, (m, pns, rT), b)
[!]
theorem wt_MethdI:
[| cmethd G C sig = Some (md, (m, pns, rT), lvars, blk, res); wf_prog G;
class G C = Some y |]
==> EX T. (G, table_of lvars(pns[|->]snd sig
) (+)¬m ?\<mapsto>Class md)|-Methd C sig:-T &
G|-T<=:rT