WellForm.thy
Back to the index of Bali_ASCII2
(* Title: isabelle/Bali/WellForm.thy
ID: $Id: WellForm.thy,v 1.10 1998/04/08 15:27:12 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 inherites more than one method with the same signature, the
methods need not have identical return types
simplifications:
* for uniformity, Object is assumed to be declared like any other class
*)
WellForm = WellType +
consts
wf_fdecl :: "prog => fdecl => bool"
wf_mhead :: "prog => sig => mhead => bool"
wf_mdecl :: "prog => tname => mdecl => bool"
wf_idecl :: "prog => idecl => bool"
wf_cdecl :: "prog => cdecl => bool"
wf_prog :: "prog => bool"
defs
(* well-formed field declaration (common part for classes and interfaces),
cf. 8.3 and (9.3) *)
wf_fdecl_def "wf_fdecl G == %(fn,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 == %(mn,pT) (pn,rT). is_type G pT &
is_type G rT & pn ~= This"
wf_mdecl_def "wf_mdecl G C == %((mn,pT),(pn,rT),lvars,blk,res).
let ltab = table_of lvars; E=(G,ltab[This|->Class C][pn|->pT])
in wf_mhead G (mn,pT) (pn,rT) &
unique lvars & ltab This = None & ltab pn = None &
(!(vn,T):set lvars. is_type G T) &
E|-blk::<> & (? T. E|-res::T & G|-T<=:rT)"
(* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3 *)
wf_idecl_def "wf_idecl G == %(I,(is,ms)).
~ is_class G I &
(!J :set is. is_iface G J) &
(!J :set is. ~ G|-J<:I I) &
(!(s,m):set ms. wf_mhead G s m) & unique ms &
(o2s o table_of ms hidings
Un_tables ((%J. (imethds G J))``set is) entails
(%(pn,rT) (md,(pn',rT')). G|-rT<=:rT'))"
(* 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 == %(C,(sc,si,fs,ms)).
~ is_iface G C &
(!I:set si. is_iface G I &
(!s. !(md',(pn',rT')) : imethds G I s.
(? md pn rT b. cmethd G C s = Some (md,((pn,rT),b)) &
G|-rT<=:rT'))) &
(!f:set fs. wf_fdecl G f) & unique fs &
(!m:set ms. wf_mdecl G C m) & unique ms &
(case sc of None => C = Object | Some D =>
is_class G D & ~ G|-D<:C C &
(table_of ms hiding cmethd G D
entails (%((pn,rT),b) (md,((pn',rT'),b')). G|-rT<=:rT')))"
(* well-formed program, cf. 8.1, 9.1 *)
wf_prog_def "wf_prog G == let is = set (fst G); cs = set (snd G) in
ObjectC : cs & (!xn. SXcptC xn : cs) &
(!i:is. wf_idecl G i) & unique (fst G) &
(!c:cs. wf_cdecl G c) & unique (snd G)"
defs
(* well-founded relations for termination proofs for iface_rec and class_rec *)
iface_wfrel_def "iface_wfrel == {((I,G, f),(I',G', f')). (G, f) = (G', f') &
wf ((subint1 G)^-1) & (I,I'):(subint1 G)^-1}"
class_wfrel_def "class_wfrel == {((C,G,tf),(C',G',tf')). (G,tf) = (G',tf') &
wf ((subcls1 G)^-1) & (C,C'):(subcls1 G)^-1}"
end
recursion operators