author | kleing |
Fri, 22 Sep 2000 16:28:53 +0200 | |
changeset 10061 | fe82134773dc |
parent 10042 | 7164dc0d24d8 |
child 10069 | c7226e6f9625 |
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 |
||
8082 | 19 |
types 'c wf_mb = 'c prog => cname => 'c mdecl => bool |
8011 | 20 |
|
21 |
constdefs |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
22 |
wf_fdecl :: "'c prog => fdecl => bool" |
10042 | 23 |
"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft" |
8011 | 24 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
25 |
wf_mhead :: "'c prog => sig => ty => bool" |
10042 | 26 |
"wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT" |
8011 | 27 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
28 |
wf_mdecl :: "'c wf_mb => 'c wf_mb" |
10042 | 29 |
"wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)" |
8011 | 30 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
31 |
wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" |
10042 | 32 |
"wf_cdecl wf_mb G == |
8011 | 33 |
\\<lambda>(C,(sc,fs,ms)). |
34 |
(\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and> |
|
8082 | 35 |
(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and> |
10042 | 36 |
(case sc of None => C = Object |
37 |
| Some D => |
|
8106 | 38 |
is_class G D \\<and> \\<not> G\\<turnstile>D\\<preceq>C C \\<and> |
8011 | 39 |
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. |
10042 | 40 |
method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))" |
8011 | 41 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
42 |
wf_prog :: "'c wf_mb => 'c prog => bool" |
10042 | 43 |
"wf_prog wf_mb G == |
8082 | 44 |
let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G" |
8011 | 45 |
|
46 |
end |