| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This chapter explains JML's notion of refinement files, which uses the following syntax.
refine-prefix ::= refine-keyword string-literal |
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
The JML tools recognize two filename suffixes: `.java' and `.jml'. See section 16.2 Using Separate Files, for guidelines on how to use these suffixes.
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).
Files with a `.jml' suffix do not have to have implementations, as they only hold specifications. In particular, one can specify methods without giving a method body in such a file.
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.
The same technique of using a file with the same base name but with a
`.jml' suffix works in such cases, as the two specifications are
added together.
For example, one might specify
the class MyType in a file named `MyType.jml'.
Then one could write the implementation of MyType in a file
called `MyType.java'.
In this example the specification found in `MyType.jml'
is a refinement of the implementation found in
`MyType.java',
and the `.jml' file is considered to follow the `.java' file
in the refinement chain.
Compilation Units that jointly give the specifications of a type form a refinement chain. It begins at a base (or most-refined) compilation unit, if it exists, and ends at the `.java' file, which 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 (i.e., directory) of the classpath is searched in order for the type's package and that contains a file whose name has a prefix matching the type name and a suffix that either (a) `.java' (or if it is up to date, `.class') or (b) `.jml'. The first up to date file of each type (a or b) is remembered and used in the chain. If it exists, the first `.jml' file found is the base of the refinement chain, otherwise the base is the the first `.java' (or `.class') file.
If there is a `.jml' file that is in the chain, then the chain has two elements and the least refined file is a `.java' (or `.class') file. Each element of the chain is in the same package.
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.jml' 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.jml' and the `Foo.java' file (as long as `Foo.jml' appears in the classpath.
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.jml', the specifications of
type B must also be in `A.jml'. 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.
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.
public, protected, private,
static, and final, must all match exactly in each such
declaration in a refinement chain.
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 refine a
non-model method with a model method. Use a spec_public or
spec_protected method if you want to use a non-model method in a
specification. Also, there may be no nesting of model declarations:
model classes and model methods may not contain model or ghost declarations.
pure, non_null, nullable, spec_public, or
spec_protected to any of the declarations for a method in any
file. However, if pure is added to a method specification,
then all subsequent declarations of that method in a refinement
sequence must also be declared pure. Also, it is, of course,
not permitted to add spec_protected to a method that has been
declared public or spec_public in other declarations.
One can add non_null or nullable to any formal parameter in any file,
although good style suggests that all of these annotations appear on
one declaration of that method.
also; if it does not an error message is issued. A
refining method declaration is a declaration that overrides a
superclass method or refines the specification of the same method in a
refinement chain. In JML, method specifications are inherited by
subclasses and in refinement chains. The also keyword
indicates that the current specification is refining the specification
inherited either from the superclass or from the previous declaration
of the method in a refinement sequence. Therefore, it is an error if
the specification of a non-refining method begins with also
(unless it overrides an inherited method).
public, protected, private, static, and
final, must all match exactly in each such declaration.
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 comment holds for ghost fields as well.
non_null, nullable, spec_public, or spec_protected to any
of the declarations for a field in any file. However, it is of
course not permitted to add spec_protected to a field that has
been declared public in other declarations.
Fields declared using the ghost modifier can have an
initializer expression in any file, but they may have at most one
initializer expression in all the files.
Model fields cannot have an initializer expression because there is no
storage associated with such fields. Use the initially clause
to specify the initial state of model fields (although the initial
state is usually determined from the represents clause).
int count is declared and there are two initially clauses,
in the same or different files, then these initially clause predicates
are conjoined; that is, both must be satisfied initially.
initializer and
static_initializer.
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].
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
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] | [ ? ] |