WellForm.thy

(*  Title:      isabelle/Bali/WellForm.thy
    ID:         $Id: WellForm.thy,v 1.2 1997/10/22 12:00:14 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)

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, (9.4), 
     representation invariants *)
  (* cf. 14.15, for scope of parameters and locals, cf. 8.4.1 and 14.3.2 *)
  wf_mhead_def	"wf_mhead G sig rT == is_type G (snd sig) &  is_type G rT"
  wf_mdecl_def	"wf_mdecl G C == %(sig,rT,blk,res). wf_mhead G sig rT & 
		(let E=(G,snd sig,C) in 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) & 
		(!(sig,mh):set ms. wf_mhead G sig mh) &  unique ms & 
		(!sig. atmost1 (Un_tables ((%J. imethd (G,J))``set is) sig)) & 
		(table ms) hiding (s2o  o  Un_tables ((%J. imethd (G,J))``set is))
		 entails (%rT (md,rT'). G|-rT<=:rT')"
(*better:
		(!sig. table ms sig = None --> 
		       atmost1## (Un_tables ((%J. imethd (G,J))``set is) sig)) & 
		(table ms) hiding (s2o##  o  Un_tables ((%J. imethd (G,J))``set is))
		         entails (%m m'. G|-snd m<=:snd m')"
*)
(*#######(!s m . imethd (G,I) s = Some  m  --> ...
        = !(s,m):set_of_table (imethd (G,I)). ....*)
  (* 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. si = Some I --> is_iface G I & 
		     (!s md  rT . imethd (G,I) s = Some (md , rT    ) --> 
		     (? b md' rT'. cmethd (G,C) s = Some (md',(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 ms) hiding (cmethd (G,D)) 
		           entails (%(rT,b) (md,(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  & 
		(!i:is. wf_idecl G i) &  unique (fst G) & 
		(!c:cs. wf_cdecl G c) &  unique (snd G)"

rules

FIXME_finite_subint1 "wf_prog G ==> finite (subint1 G)"
FIXME_finite_subcls1 "wf_prog G ==> finite (subcls1 G)"

end