1 (* Title: HOL/MicroJava/J/WellType.thy |
1 (* Title: HOL/MicroJava/J/WellType.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb |
3 Author: David von Oheimb |
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 |
5 *) |
6 Well-typedness of Java programs |
6 |
7 |
7 header "Well-typedness Constraints" |
|
8 |
|
9 theory WellType = Term + WellForm: |
|
10 |
|
11 text {* |
8 the formulation of well-typedness of method calls given below (as well as |
12 the formulation of well-typedness of method calls given below (as well as |
9 the Java Specification 1.0) is a little too restrictive: Is does not allow |
13 the Java Specification 1.0) is a little too restrictive: Is does not allow |
10 methods of class Object to be called upon references of interface type. |
14 methods of class Object to be called upon references of interface type. |
11 |
15 |
12 simplifications: |
16 \begin{description} |
13 * the type rules include all static checks on expressions and statements, e.g. |
17 \item[simplifications:]\ \\ |
14 definedness of names (of parameters, locals, fields, methods) |
18 \begin{itemize} |
15 |
19 \item the type rules include all static checks on expressions and statements, |
16 *) |
20 e.g.\ definedness of names (of parameters, locals, fields, methods) |
17 |
21 \end{itemize} |
18 theory WellType = Term + WellForm: |
22 \end{description} |
19 |
23 *} |
20 types lenv (* local variables, including method parameters and This *) |
24 types lenv (* local variables, including method parameters and This *) |
21 = "vname \<leadsto> ty" |
25 = "vname \<leadsto> ty" |
22 'c env |
26 'c env |
23 = "'c prog \<times> lenv" |
27 = "'c prog \<times> lenv" |
24 |
28 |