1 (* Title: HOL/MicroJava/J/WellForm.thy
3 Author: David von Oheimb
4 Copyright 1999 Technische Universitaet Muenchen
6 Well-formedness of Java programs
7 for static checks on expressions and statements, see WellType.thy
9 improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
10 * a method implementing or overwriting another method may have a result type
11 that widens to the result type of the other method (instead of identical type)
14 * for uniformity, Object is assumed to be declared like any other class
19 types 'c wtm = 'c prog => cname => 'c mdecl => bool
23 wf_fdecl :: "'c prog \\<Rightarrow> fdecl \\<Rightarrow> bool"
24 "wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft"
26 wf_mhead :: "'c prog \\<Rightarrow> sig \\<Rightarrow> ty \\<Rightarrow> bool"
27 "wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
29 wf_mdecl :: "'c wtm \\<Rightarrow> 'c wtm"
30 "wf_mdecl wtm G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wtm G C (sig,rT,mb)"
32 wf_cdecl :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
33 "wf_cdecl wtm G \\<equiv>
34 \\<lambda>(C,(sc,fs,ms)).
35 (\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and>
36 (\\<forall>m\\<in>set ms. wf_mdecl wtm G C m) \\<and> unique ms \\<and>
37 (case sc of None \\<Rightarrow> C = Object
38 | Some D \\<Rightarrow>
39 is_class G D \\<and> \\<not> G\\<turnstile>D\\<prec>C C \\<and>
40 (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
41 method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
43 wf_prog :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
44 "wf_prog wtm G \\<equiv>
45 let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wtm G c) \\<and> unique G"