author | oheimb |
Wed, 06 Dec 2000 19:10:36 +0100 | |
changeset 10613 | 78b1d6c3ee9c |
parent 10069 | c7226e6f9625 |
child 11026 | a50365d21144 |
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 |
|
10069 | 22 |
wf_fdecl :: "'c prog => fdecl => bool" |
10042 | 23 |
"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft" |
8011 | 24 |
|
10069 | 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 == |
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10069
diff
changeset
|
33 |
\\<lambda>(C,(D,fs,ms)). |
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10069
diff
changeset
|
34 |
(\\<forall>f\\<in>set fs. wf_fdecl G f) \\<and> unique fs \\<and> |
10069 | 35 |
(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and> |
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10069
diff
changeset
|
36 |
(C \\<noteq> Object \\<longrightarrow> is_class G D \\<and> \\<not>G\\<turnstile>D\\<preceq>C C \\<and> |
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10069
diff
changeset
|
37 |
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. |
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10069
diff
changeset
|
38 |
method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))" |
8011 | 39 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
40 |
wf_prog :: "'c wf_mb => 'c prog => bool" |
10042 | 41 |
"wf_prog wf_mb G == |
8082 | 42 |
let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G" |
8011 | 43 |
|
44 |
end |