author | nipkow |
Fri, 26 Nov 1999 08:46:59 +0100 | |
changeset 8034 | 6fc37b5c5e98 |
parent 8011 | d14c4e9e9c8e |
child 8082 | 381716a86fcb |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/WellForm.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
Well-formedness of Java programs |
|
7 |
for static checks on expressions and statements, see WellType.thy |
|
8 |
||
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) |
|
12 |
||
13 |
simplifications: |
|
14 |
* for uniformity, Object is assumed to be declared like any other class |
|
15 |
*) |
|
16 |
||
17 |
WellForm = TypeRel + |
|
18 |
||
19 |
types 'c wtm = 'c prog => cname => 'c mdecl => bool |
|
20 |
||
21 |
constdefs |
|
22 |
||
23 |
wf_fdecl :: "'c prog \\<Rightarrow> fdecl \\<Rightarrow> bool" |
|
24 |
"wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft" |
|
25 |
||
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" |
|
28 |
||
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)" |
|
31 |
||
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'. |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8011
diff
changeset
|
41 |
method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))" |
8011 | 42 |
|
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" |
|
46 |
||
47 |
end |