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

16. Refinement

This chapter explains JML's notion of refinement files, which uses the following syntax.

 
refine-prefix ::= refine-keyword string-literal ;
refine-keyword ::= refine | refines

The refine-prefix in a compilation unit says that the declarations in this compilation unit refine the corresponding declarations in the file named by the string-literal. The string-literal should name a file, complete with a suffix, for example, "MyType.java-refined". The suffix of such a file is used by JML tools to find the file that is the base of a refinement chain, and all other files in the chain are found using the files named in the refine-prefix of a previous file in the chain.

One can use either keyword, refine or refines in a refine-prefix, although for historical reasons most examples use refine.

The following gives more details about the checks and meaning of this feature of JML.

16.1 File Name Suffixes  
16.2 Using Separate Files  
16.3 Refinement Chains  
16.4 Type Checking Refinements  
16.5 Refinement Viewpoints  


16.1 File Name Suffixes

The JML tools recognize several filename suffixes. The following are considered to be active suffixes: `.refines-java', `.refines-spec', `.refines-jml', `.java', `.spec', and `.jml'; There are also three passive suffixes: `.java-refined', `.spec-refined', and `.jml-refined'. Files with passive suffixes can be used in refinements but should not normally be passed explicitly to the tools directly. These filename suffixes are ordered from most active to least active, in the order given above. Graphical user interface tools for JML should, by default, only present the active suffixes for selection. Among files in a directory with the same prefix, but with different active suffixes, the one whose suffix appears first in the list of active suffixes above should be considered primary by such a tool.

See section 16.2 Using Separate Files, for guidelines on how to use these suffixes. See section 16.3 Refinement Chains, for details on the semantics of specifications written using separate files.


16.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 an active suffix, such as `.refines-java' (or `.refines-spec' or `.refines-jml'). 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.refines-java', and include in that file the following refine-prefix.

 
  refine "LibraryType.java";

If you are specifying code for which no sources are available (a class library in binary form), then you should use the `.spec' or `.jml' suffixes to write the specification. Such specifications act much like those written in `.refines-spec' or `.refines-jml' files, but would not include a refine-prefix. They allow specifications to be written without having to write Java code for the bodies of methods (as do all non-`.java') files.

Another reason for writing specifications in different files is to prevent the specifications from "cluttering up" the code (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. In such a case one has a choice of suffixes, depending on whether one considers the code to be primary or the specification. If the code is primary, or has been written already, then one can treat the code as if it were written in an extra library, using the `.refines-java' (or `.refines-spec' or `.refines-jml') suffixes to specify the Java files as above.

On the other hand, if the specification is primary, or is to be written first, one could instead use the `.java-refined' (or `.spec-refined' or `.jml-refined') suffixes, and then write a refine-prefix in the `.java' file. For example, one might specify the class MyType in a file named `MyType.java-refined'. Then one could write the implementation of MyType in a file called `MyType.java'. The file `MyType.java' would include the following refine-prefix:

 
  refine "MyType.java-refined";

In this case, the specification found in `MyType.java-refined' is a refinement of the implementation found in `MyType.java'.

Combinations of these techniques can also be used, by using several files instead of just a code file and a specification file. See section 16.3 Refinement Chains, for the meaning of JML specifications in this general case.

To summarize, aside from the standard `.java' suffix, one would use file name suffixes as follows.


16.3 Refinement Chains

Compilation Units that jointly give the specifications of a type form a refinement chain. It begins at a base (or most-refined) compilation unit, proceeding by means of the refine annotation links, until a file is found that has no refine statement. That file is the end of the refinement chain and is the least-refined compilation unit.

For a given type in a given package, the base of the refinement chain is found as follows. Each entry of the classpath is searched in order for a directory whose name matches the package of the type and that contains a file whose name has a prefix matching the type name and a suffix that is an active suffix as defined above. The first such file found is the base of the refinement chain. If the first classpath entry to contain a candidate file contains more than one candidate file, then the file with the most active suffix is the base of the chain.

The subsequent elements of the refinement chain are given by the filenames provided in the refine statements. Each element of the chain is in the same package. Thus the file corresponding to the refine statement is the first file found by searching the classpath entries in order and that is in the directory corresponding to the package of the type and has the filename and suffix given in the refine statement.

To help ensure that the base is correctly selected, the file with the most active suffix must be the base of a refinement sequence, otherwise the JML typechecker issues an error message. Also, the prefix of the base file must be the same as the public type declared in that compilation unit or an error message is issued. However, it is not necessary that the file being refined have the same prefix as the file at the base of the refinement chain (except that the .java file, if it is in the refinement sequence, must have a name given by the Java rules for naming compilation units). Furthermore, a file with the same prefix as the base file may not be in a different refinement sequence. For example, `SomeName.java-refined' can be refined by `MyType.java' as long as there is no refinement sequence with `SomeName' as the prefix of the base of another refinement.

The JML tools deal with all files in a refinement chain whenever one of them is selected for processing by the tool. This allows all of the specifications that apply to be consistently dealt with at all times. For example, suppose that there are files named `Foo.refines-java' and `Foo.java', then if a tool selects the `Foo.java', e.g., with the command:

 
   jmlc *.java

then it will see both the `Foo.refines-java' and the `Foo.java' file (as long as `Foo.refines-java' appears in a specification path directory before or with `Foo.java').

A given .java file (that is, compilation unit) may have more than one top-level class declaration within it. Only one may be public, and Java requires that the name of that type match the name of the file, so that the definition of the type can be found in the file system. The non-public types within that compilation unit may be referred to only within that compilation unit. Consequently, all specifications of those non-public types must occur along with the specifications of the public type in that compilation unit. For example, suppose a file `A.java' contains the Java declaration of types A and B. Then if the specifications of type A are in `A.refines-java', the specifications of type B must also be in `A.refines-java'. For simple one-file programs, the one compilation unit may contain only non-public types. Then the specifications for those types are found in specification files with the same prefix as the filename of the Java file containing the type declarations.


16.4 Type Checking Refinements

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

JML uses specification inheritance to impose the specifications of supertypes on their subtypes [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b] to support the concept of behavioral subtyping [America87] [Leavens90] [Leavens91] [Leavens-Weihl90] [Leavens-Weihl95] [Liskov-Wing94]. JML also supports a notion of weak behavioral subtyping [Dhara-Leavens94b] [Dhara97].


16.5 Refinement Viewpoints

In refinements, specification inheritance allows the specifier to separate the public, protected, and private specifications into different files. Public specifications give the public behavior and are meant for clients of the class. Protected specifications are meant for programmers creating subclasses and give the protected behavior of the type; they give the behavior of protected methods and fields that are not visible to clients. Similarly, private specifications are meant for implementors of the class and provide the behavior related to private methods and fields of the class; implementors must satisfy the combined public, protected, and private specifications of a method.

[[[Needs work]]]

16.5.1 Default Constructor Refinement  


16.5.1 Default Constructor Refinement

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' (the same constructor is generated as in the Java language). Consider, for example, the refinement sequence defined by the following three files, RefineDemo.jml-refined, RefineDemo.jml, and RefineDemo.java.

 
// ---- file RefineDemo.jml-refined ---
package org.jmlspecs.samples.jmlrefman;

public class RefineDemo {
   //@ public model int x;

   /*@ public normal_behavior
     @    assignable x;
     @    ensures x == 0; @*/
   public RefineDemo();
}

 
// ---- file RefineDemo.jml -----------
package org.jmlspecs.samples.jmlrefman;

//@ refine "RefineDemo.jml-refined"; 

public class RefineDemo {
   protected int x_; 
   //@           in x;

   //@ protected represents x <- x_;
}

 
// ---- file RefineDemo.java ---------
package org.jmlspecs.samples.jmlrefman;

//@ refine "RefineDemo.jml"; 

public class RefineDemo {
   protected int x_; 
   public RefineDemo() { x_ = 0; }
}

In the protected specification declared in `RefineDemo.jml', no constructor is defined. If JML were to generate a default constructor for this class declaration, then the public constructor defined earlier in the refinement chain, in `RefineDemo.jml-refined', could have a visibility modifier that conflicts with the one automatically generated for the protected specification. (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.) Recall that the signature, including the visibility modifier, must match for every method and constructor declared in a refinement chain. To avoid such conflicts, JML does not generate a default constructor unless the file suffix is `.java' (as part of the standard compilation process).

A similar problem can occur when the only constructor is protected or private as in the refinement sequence defined by the following three files, RefineDemo2.jml-refined, RefineDemo2.jml, and RefineDemo2.java.

 
// ---- file RefineDemo2.jml-refined --
package org.jmlspecs.samples.jmlrefman;

public class RefineDemo2 {
   //@ public model int x;
   //@ public initially x == 0;
}

 
// ---- file RefineDemo2.jml ----------
package org.jmlspecs.samples.jmlrefman;

//@ refine "RefineDemo2.jml-refined"; 
public class RefineDemo2 {
   protected int x_; 
   //@           in x;

   //@ protected represents x <- x_;

   /*@ protected normal_behavior
     @    assignable x;
     @    ensures x == 0; @*/
   protected RefineDemo2();
}

 
// ---- file RefineDemo2.java ---------
package org.jmlspecs.samples.jmlrefman;

//@ refine "RefineDemo2.jml"; 
public class RefineDemo2 {
   protected int x_; 
   protected RefineDemo2() { x_ = 0; }
}

In this example, notice that no constructor is defined for the public specification in `RefineDemo2.jml-refined'. If a default constructor were generated for this class declaration, then the protected constructor defined later in the refinement chain, in `RefineDemo2.jml', would have a visibility modifier that conflicts with the one automatically generated and JML would emit an error. Thus JML only generates the default constructor for the executable declaration of a class in the `.java' file and only when required by the Java language.


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

This document was generated by Gary Leavens on March, 16 2009 using texi2html