[ << ] | [ >> ] | [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 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.
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.
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.
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] | [ ? ] |