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

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.


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.)


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

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