| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
A compilation unit in JML is similar to that in Java, with some additions. It has the following syntax.
compilation-unit ::= [ package-definition ]
[ refine-prefix ]
[ import-definition ] ...
[ top-level-definition ] ...
top-level-definition ::= type-definition
| multijava-top-level-declaration // When parsing MultiJava
|
The compilation-unit rule is the start rule for the JML grammar. (In this syntactic rule and in all other rules in the rest of the body of this manual, white-space may appear between any two tokens. See section 4. Lexical Conventions, for details.)
See section 6. Type Definitions, for the syntax and semantics of type-definitions. See section 17.1 Augmenting Method Declarations, for the syntax and semantics of multijava-top-level-declaration. See section 16. Refinement, for a discussion of the refine-prefix and its uses.
Some JML tools may support various optional extensions to JML. This manual partially describes two such extensions: MultiJava [Clifton-etal00] and the Universe type system [Dietl-Mueller05]. Comments in the grammar indicate optional productions; these are only used by tools that select an option to parse the syntax in question. Tools for JML do not have to support these extensions to JML, and may themselves support other JML extensions. In general, JML tools will support a (hopefully well-documented) variant of the language described in this manual.
The Java code in a compilation unit must be legal Java code (or legal
code in the Java extension, such as MultiJava, selected by any options);
in particular it must obey all of Java's static restrictions.
For example, at most one of the type definitions in a compilation unit
may be declared public.
See the Java Language Specification [Gosling-etal00]
for details.
As in Java, JML can be implemented using files to store compilation units. When this is done there must also be a correspondence between the name of any public type defined in a compilation unit and the file name. This is done exactly as in Java, although JML allows additional file name suffixes. See section 16.1 File Name Suffixes, for details on the file name suffixes allowed in JML.
The specification of the compilation unit consists of the
specifications of the top-level-definitions it contains, placed in
the declared package (if any). The interface part of this specification is
determined as in Java [Gosling-etal00] (or as in the Java extension used).
The specifications of each type-definition are computed by starting
from an environment that contains the declared package (if any),
each top-level definition in the compilation unit (to allow for
mutual recursion), and the imports [Gosling-etal00].
In JML, not only is the package java.lang implicitly imported, but also
there is an implicit model import of org.jmlspecs.lang.
(See section 5.2 Import Definitions, for the meaning of a model import.)
Ignoring refinement, a Java compilation unit satisfies such a JML specification if it satisfies the specified package-definition (if any), and if for each specified type-definition, there is a corresponding Java type-definition that satisfies that type's JML specification. Furthermore, if the JML specification does not contain a public type, then the Java compilation unit may not contain a public type.
The syntax and semantics of package-definitions and import-definitions are discussed in the subsections below.
5.1 Package Definitions 5.2 Import Definitions
The syntax of a package-definition is as in Java [Gosling-etal00].
package-definition ::= |
A Java package definition satisfies the JML specification only if it is the same as that specified. That is, the Java code has to be the same (modulo white-space) as the JML specification.
The syntax of a import-definition is as follows.
The only difference from the Java syntax [Gosling-etal00]
is the optional model modifier.
import-definition ::= [ |
An import-definition may use the model modifier
if and only if the whole import-definition is entirely contained
within a single annotation. For example, the following is illegal.
|
To write an import that affects both the JML annotations and Java
code, just use a normal java import, without using the model
modifier.
The effect on the interface computed for a compilation unit of an
import-definition without the model
keyword is the same as in Java [Gosling-etal00]. Such import
directives affect the computation of the interface of the Java code as
well as the JML specification (that is, they apply to both equally).
When the model keyword is used,
the import only has an effect on the JML annotations (and not on the
Java code). The abbreviation permitted by the use of such an import,
however, is the same as would be effected by a normal Java import.
Such model imports can affect the computation of the interface
of the JML specification by being used in the declarations of model
and ghost features.
Both normal Java and model imports do not themselves contribute to the interface of a JML specification. As such, they do not have to be present in a correct implementation of the specification. An implementation could, for example, use different forms of import, or it could use fully qualified names instead of imports, and achieve the same effect as using the imports in the specification.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |