| [ << ] | [ >> ] | [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-declaration ]
[ import-declaration ] ...
[ top-level-declaration ] ...
top-level-declaration ::= type-declaration
|
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 Declarations, for the syntax and semantics of type-declarations.
See section 17. Separate Files for Specifications, for a discussion of how you can place JML
specification in separate (.jml) files.
Some JML tools may support various optional extensions to JML. This manual partially describes one such extension: 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 the Universe type system,
selected by any options);
in particular it must obey all of Java's static restrictions.
For example, at most one of the type declarations in a compilation unit
may be declared public.
See the Java Language Specification [Gosling-etal05]
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 17.1 File Name Suffixes, for details on the file name suffixes allowed in JML and how the extra files determine the specification for the compilation unit.
The specification of the compilation unit consists of the
specifications of the top-level-declarations it contains, placed in
the declared package (if any). The interface part of this specification is
determined as in Java [Gosling-etal05] (or as in the Java extension used).
The specifications of each type-declaration 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-etal05].
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 Declarations, for the meaning of a model import.)
A Java compilation unit satisfies such a JML specification if it satisfies the specified package-declaration (if any), and if for each specified type-declaration, there is a corresponding Java type-declaration 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-declarations and import-declarations are discussed in the subsections below.
5.1 Package Declarations 5.2 Import Declarations
The syntax of a package-declaration is as in Java (see Section 7.4 of [Gosling-etal05]). See section 6.2.2 Java Annotations, for the syntax of java-annotations.
package-declaration ::= [ java-annotations ] |
A Java package declaration satisfies the JML specification only if its java-annotations are satisfied by the declaration and if the remainder of the package declaration 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-declaration is as follows.
The only difference from the Java syntax [Gosling-etal05]
is the optional model modifier.
import-declaration ::= [ |
An import-declaration may use the model modifier
if and only if the whole import-declaration 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-declaration without the model
keyword is the same as in Java (Section 7.5 of [Gosling-etal05]).
Checking of such
import declarations is done exactly as in Java. Such import
declarations 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] | [ ? ] |