[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

5. Compilation Units

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  

5.1 Package 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 ] package name ;
name ::= ident  [ . ident ] ...

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.

5.2 Import Declarations

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 ::= [ model ] import [ static ] name-star ;
name-star ::= ident [ . ident ] ... [ . * ]

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.

/*@ model @*/ import com.foo.*; // 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] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html