17. Separate Files for Specifications

This chapter explains how to use separate files to hold JML specifications.

The following gives more details about this feature of JML.

17.1 File Name Suffixes
17.2 Using Separate Files
17.3 Type Checking Separate Files
17.4 Default Constructors and Separate Files

17.1 File Name Suffixes

The JML tools recognize three filename suffixes: `.java', `.class', and `.jml'. See section 17.2 Using Separate Files, for guidelines on how to use these suffixes.

17.2 Using Separate Files

Typically, JML specifications are written into annotation comments in `.java' files, and this is certainly the simplest way to use JML and its tools.

However, there are some circumstances in which one may wish to separate the specification from the Java code. An important example of this is when you do not own the sources for the Java code, but wish to specify it. This might happen if you are specifying a class library or framework that you are using. When you do not have control of the code, it is best to put the specification in a different file.

To add specifications to such a library or framework, one would use a filename with a `.jml' suffix. The file with such a name would hold the specifications of the corresponding Java compilation unit. For example, if one wants to specify the type LibraryType, without touching the file `LibraryType.java' then one could write specifications in the file `LibraryType.jml'. This technique also works if you are specifying code for which no sources are available (a class library in binary form).

Note that the `.jml' file should contain all the (non-inherited) specifications for the types in the compilation unit; there should be no specifications at all in the `.java' file. Thus, in our example, there should be no JML specifications at all in the `LibraryType.java' file, and all the specifications should be found in the `LibraryType.jml' file.

Files with a `.jml' suffix do not have to have implementations, as they only hold specifications. In particular, in such a file one can and must specify non-model methods without giving a method body.

Another reason for writing specifications in different files is to prevent the specifications from "cluttering up" the code (i.e., making it hard to see all of the code at once). This is also possible by using separate files for the specification and the code. The same technique of using a file with the same base name but with a `.jml' suffix works in such cases, as the specifications in the `.jml' file are added to the code in the `.java' file.

17.3 Type Checking Separate Files

There are some restrictions on what can appear in a separate specification file (i.e., in the `.jml' file). Since the Java compilers only see the `.java' files, executable code (that is not just for use in specifications) can only be placed in the `.java' files. In particular the following restrictions are enforced by JML.

• When the same method is declared in more than one file, most parts of the method declaration must be identical in all the files. (Two method declarations are considered to be declaring the same method if they have the same signature, i.e., same name, same generic type parameters, and static formal parameter types.) However, in addition to the signature of such a method, the return type, the names of the formal parameters, the declared exceptions the method may throw, and the non-JML modifiers public, protected, private, static, and final, must all match exactly in each such pair of matching declarations.

• The model modifier must appear in all declarations of a given method or it must appear in none of them. It is not permitted to implement a model method with a non-model method or to specify a non-model method as a model method. Use a pure spec_public or spec_protected method if you want to use a non-model method in a (public or protected) specification. Also, there may be no nesting of model declarations: model classes and model methods may not contain model declarations.

• Some of the JML method modifiers do not always have to match in all declarations of the same method found in separate files. One may add pure, non_null, nullable, spec_public, or spec_protected to any of the declarations for a method in any file. Also, it is, of course, not permitted to add spec_protected to a method that has been declared public or spec_public in the other declaration. One can add non_null or nullable to any formal parameter in a separate (`.jml') file.

• The specification of a method declaration in a separate file is the only specification of that method. Therefore, unless that method is overriding a method in a supertype, it should not start with the JML keyword also. In such a case, the also is a clue to the reader that the specification is adding to a possibly inherited specification, either from the superclass or from an implemented interface. Therefore, it is an error if the specification of a non-overriding method begins with also, regardless of whether it is in a separate file. (See section B. Incompatible Changes, for how this is different than earlier versions of JML.)

• If a non-model method has a body, then the body can only appear in a `.java' file; an error message is issued if the body of a non-model method appears in a file with any other suffix. Furthermore, the body of a model method may only appear in one file; thus, if there is a `.jml' file, then the body of the model method must appear (if it appears at all) in the `.jml' file. Thus each method of each class can have at most one method body.

• When the same field is declared in more than one file, then the signature of each such declaration must be identical in all the files. (Two field declarations in a given type are considered to be declaring the same field if they have the same name.) The signature of such a field, including its type, the non-JML modifiers public, protected, private, static, and final, must all match exactly in each such pair of matching declarations.

• All declarations of a given field must either use the modifier model or not. It is not permitted to implement a model field with a non-model field or vice versa. Use a spec_public or spec_protected field if you want to use the same name. The same restriction also holds for ghost fields.

• One may add non_null, nullable, spec_public, or spec_protected to any of the declarations for a field in a separate file. However, it is of course not permitted to add spec_protected to a field that has been declared public in another declaration.

• Initializers are not allowed for field declarations in separate specification files. A non-model and non-ghost field can have an initializer expression, but this initializer can only appear in a `.java' file because this is where a compiler expects to find it.

  Fields declared using the ghost modifier can have an initializer expression in a separate specification file, but they may have at most one initializer expression. Thus, if there is a separate specification file, the initializer for a ghost field must appear there.

  Model fields cannot have an initializer expression because there is no storage associated with such fields. If you want to specify initial values for a model field in a separate file, then use the initially clause in that file.

• An initializer block or a static initializer block (with code) may only appear in a `.java' file. One can write annotations to specify the effects of such initializers in JML annotations in other files, using the keywords initializer and static_initializer. Such specifications may only appear in one file, and thus if there is a separate specification (`.jml') file, it must appear in that file.

17.4 Default Constructors and Separate Files

In Java, a default constructor is automatically generated for a class when no constructors are declared in a class. However, in JML, a default constructor is not generated for a class unless the file suffix is `.java' (where the same constructor is generated as in the Java language). Consider, for example, the refinement sequence defined by the following two files: RefineDemo.jml and RefineDemo.java.

// ---- file RefineDemo.jml ----------- package org.jmlspecs.samples.jmlrefman; public class RefineDemo { //@ public model int x; protected int x_; //@ in x; //@ protected represents x = x_; }

// ---- file RefineDemo.java --------- package org.jmlspecs.samples.jmlrefman; public class RefineDemo { protected int x_; public RefineDemo() { x_ = 0; } }

In the protected specification declared in `RefineDemo.jml', no constructor is specified. The reason that JML does not generate a default constructor for such separate specification files is that it might conflict with the constructor explicitly declared in the `.java' file. To see why, consider what would happen if JML were to generate a default constructor for RefineDemo for the `RefineDemo.jml' file. If JML did that, then this default constructor would possibly have a different visibility from any constructor written explicitly in the `RefineDemo.java' file. To avoid such conflicts, JML does not generate a default constructor unless the file suffix is `.java'.

(The visibility modifier of an automatically-generated default constructor depends on other factors including the visibility of the class. See section 9.4 Lightweight Specification Cases, for more details.)