|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|
The nonterminal field describes all the members of classes and interfaces (see section 6.1 Class and Interface Definitions).
field ::= member-decl | jml-declaration | class-initializer-decl |
Also see section E.2.1 Non-null by Default. In the rest of this chapter we describe mostly the syntax and Java details of member declarations and class initializers. See section 8. Type Specifications, for the syntax and semantics of jml-declaration, and, more generally, how to use JML to specify the behavior of types.
The following gives the syntax of Java member declarations.
member-decl ::= method-decl | variable-definition | class-definition | interface-definition
See section 6.1 Class and Interface Definitions, for details of class-definition and interface-definition. We discuss method and variable declarations below.
The following is the syntax of a method declaration.
method-decl ::= [ doc-comment ] ... method-specification modifiers [ method-or-constructor-keyword ] [ type-spec ] method-head method-body | [ doc-comment ] ... modifiers method-or-constructor-keyword [ type-spec ] method-head [ method-specification ] method-body method-or-constructor-keyword ::=
Notice that the specification of a method (see section 9. Method Specifications) may appear either before or after the method-head.
The use of
non_null as a modifier in a method-decl
really is shorthand for a postcondition describing the normal result
of a method, indicating that it must not be null. It can also be seen as a
modifier on the method's result type, saying that the type
returned does not contain null.
The use of
extract as a modifier in a method-decl
is shorthand for writing a model program specification.
See section 14.2 Extracting Model Program Specifications, for an explanation of
18.104.22.168 Formal Parameters 22.214.171.124 Model Methods and Constructors 126.96.36.199 Pure Methods and Constructors 188.8.131.52 Helper Methods and Constructors
See section 184.108.40.206 Type-Specs, for more about the nonterminals type-spec and dims. See section 17.2 MultiMethods, for details of multijava-param-declaration.
non_null when attached to a formal parameter is
shorthand for a precondition that says that the corresponding actual
parameter may not be null. The type of a parameter that has the
non_null modifier must be a reference type
non_null modifier on a parameter is inherited in the same
way as the equivalent precondition would be, so it need not be
declared on every declaration of the same method in a subtype or refinement.
non_null modifier may be added to a method in a refinement
file (see section 16. Refinement), and thus does not have to appear in any
particular file in a refinement sequence. It can be added to a method
override in a subtype, but that will generally make the method
non-implementable, as the method must also satisfy an inherited
specification without the corresponding precondition.
A method or constructor that uses the modifier
model is called
a model method or constructor.
Since a model method is not visible to Java code, the entire method,
including its body, should be written in an annotation.
As usual in JML (see section 2.2 Model and Ghost), a model method or constructor is a specification-only feature. A model method or constructor may have either a body or a specification, or both. The specification may be used in various verification tools, while the body allows it to be executed during runtime assertion checking. Model methods may also be abstract, and both model methods and constructors may be final.
[[[ Can constructors be final? Why? - DRC ]]]
It is usual in JML to declare model methods and constructors as
pure. However, it is possible to have a model method or
constructor that is not pure; such methods are useful in model
programs (see section 14. Model Programs).
On the other hand, aside from their use in model programs, most model
methods only exist to be called in assertions, and since only
pure methods can be called in assertions, they should usually be
This subsubsection, which describes the effect of the
on methods and constructor declarations, is quoted from the preliminary design
We say a method
is pure if it is either specified with
pure or is a method that
appears in the specification of a
pure interface or class.
Similarly, a constructor is pure if it is either specified with
pure or appears in the specification of a
A pure method that is not a constructor implicitly has a specification that does not allow any side-effects. That is, its specification has the clauses
diverges false; assignable \nothing;
A pure constructor has the clauses
diverges false; assignable this.*;
Implementations of pure methods and constructors will be checked to see that they meet these conditions on what locations they can assign to. To make such checking modular, some JML tools prohibit a pure method or constructor implementation from calling methods or constructors that are not pure. However, more sophisticated tools could more directly check the intended semantics [Salcianu-Rinard05].
A pure method or constructor must also be provably terminating. Although JML does not force users to make such proofs of termination, users writing pure methods and constructors are supposed to make pure methods total in the sense that whenever, a pure method is called it either returns normally or throws some exception. This is supposed to lessen the possibility that assertion evaluation could loop forever, aids the runtime assertion checker, which turns exceptions into arbitrary values of the appropriate result type, and helps make pure methods more like mathematical functions for verification purposes. [[[ I think this has changed - exceptions in a pure method make the result undefined, not arbitrary - DRC]]]
Furthermore, a pure method is supposed to always either terminate normally or throw an exception, even for calls that do not satisfy its precondition. Static verification tools for JML should enforce this condition, by requiring a proof that a pure method implementation satisfies the following specification
private behavior requires true; diverges false; assignable \nothing;
assignable this.*;for constructors).
However, this implicit verification condition is a specification, and thus cannot be used in reasoning about calls to the method, even calls from within the class itself and recursive calls from within the implementation. For this reason we recommend writing the method or constructor specification in such a way that the effective precondition of the method is "true," making the proof of the above implicit verification condition trivial, and allowing the termination behavior of the implementation to be relied upon by all clients.
Recursion is permitted, both in the implementation of pure methods
and the data structures they manipulate, and in the specifications of
When recursion is used in a specification,
the proof of well-formedness for the specification
involves the use of JML's
Since a pure method may not go into an infinite loop, if it has a non-trivial precondition, it should throw an exception when its normal precondition is not met. This exceptional behavior does not have to be specified or programmed explicitly, but technically there is an obligation to meet the specification that the method never loops forever.
Furthermore, a pure method must be deterministic, in the sense that when called in a given state, it must always return the same value. Similarly a pure constructor should be deterministic in the sense that when called in a given state, it always initializes the object in the same way.
A pure method can be declared in any class or interface, and a pure constructor can be declared in any class. JML will specify the pure methods and constructors in the standard Java libraries as pure.
As a convenience, instead of writing
pure on each
method declared in a class and interface,
one can use the modifier
pure on classes and
interfaces and classes.
This simply means that each non-static method and each constructor
declared in such a class or interface is
Note that this does not mean that all methods inherited (but not
declared in and hence not overridden in) the class or interface are
For example, every class inherits ultimately from
which has some methods, such as
that are manifestly not pure.
Thus each class will have some methods that are not pure.
Despite this, it is convenient to refer to classes and interfaces declared
pure modifier as pure.
In JML the modifiers
are orthogonal. (Recall something declared with
model does not have to be
implemented, and is used purely for specification purposes.)
Therefore, one can have a model method
that is not pure (these might be useful in JML's model programs)
and a pure method that is not a model method.
Nevertheless, usually a model method (or constructor) should be pure,
since there is no way to use non-pure methods in an assertion,
and model methods cannot be used in normal Java code.
By the same reasoning, model classes should, in general, also be pure. Model classes cannot be used in normal Java code, and hence their methods are only useful in assertions (and JML's model programs). Hence it is typical, although not required, that a model class also be a pure class.
As can be seen from the semantics,
if a pure method has a return type of
void, then it can
essentially only do nothing. So, while pure methods
void as their return type are not illegal, they are
helper modifier may only be used on a private method or
constructor. [[[ This restriction needs to be clarified - ESC/Java limits
helper to non-overridable methods. ]]] Such a helper method or constructor has a
specification that is not augmented by invariants and history constraints
that would otherwise apply to it. It can thus be thought of as not
really a method or constructor, but merely an abbreviation device.
However, whatever specifications are given explicitly for such a
method or constructor still apply.
See section 8.2 Invariants, for more details.
The following is the syntax of field and variable declarations.
variable-definition ::= [ doc-comment ] ... modifiers variable-decls variable-decls ::= [
field keyword is not normally needed, but can be used to
change JML's parsing mode. Within an annotation, such as within a
declaration of a model method, it is sometimes necessary to switch
from JML annotation mode to JML spec-expression mode, in order to
parse words that are JML keywords but should be recognized as Java
identifiers. This can be accomplished in a field declaration by using
field, which changes parsing to spec-expression
mode. [[[ When does the mode revert back? e.g. in a method declaration - DRC]]]
[[[Needs example, move elsewhere?]]]
In a non-Java file, such as a file with suffix `.refines-java'
(see section 16. Refinement), one
may omit the initializer of a variable-declarator, even one
declared to be
final. In such a file, one may also omit the body
of a method-decl. Of course, in a `.java' file, one must
obey all the rules of Java for declarations that are not in annotations.
See section 10. Data Groups, for more about jml-data-group-clauses. See section 11.2 Specification Expressions, for the syntax of expression. In the following we discuss the modifiers for field and variable declarations and type-specs.
model modifiers for fields both say that
the field is a specification-only field; it thus cannot be accessed by
the Java code. The difference is that a ghost field is explicitly
manipulated by initializations and set statements
(see section 12. Statements and Annotation Statements),
whereas a model field cannot be explicitly manipulated. Instead a
model field is indirectly given a value by a represents clause
(see section 8.4 Represents Clauses).
See section 2.2 Model and Ghost, for a general discussion of this distinction in
While fields can be declared as either model or ghost fields, a field
cannot be both. Furthermore, local variables cannot be declared with
non_null modifier in a variable declaration is shorthand
for an invariant saying that each variable declared in the
variable-decls may not be null. This invariant has the same
visibility as the visibility declaration of the
variable-definition itself. See section 8.2 Invariants, for more about
monitored modifier says that each variable declared in the
variable-decls can only be accessed by a thread that holds the lock
on the object that contains the field
It may not be used with model fields.
instance modifier says that the field is to be found in
instances instead of in class objects; it is the opposite of
static. It is typically only needed for model or ghost fields
declared in interfaces. When used in an interface, it makes the field
both non-static and non-final (unless the
final modifier is
See section 2.5 Instance vs. Static.
[[[ So how does one declare a static non-final field in an interface? - DRC ]]]
The syntax of a type-spec is as in Java [Gosling-etal00],
except for the addition of the type
\TYPE and the possibility
of using ownership-modifiers.
The ownership-modifiers are only available when the Universe
type system is turned on. See section 18. Universe Type System, for how to do
that, and for the syntax and semantics of ownership-modifiers.
type-spec ::= [ ownership-modifiers ] type [ dims ] |
\TYPE represents the kind of all Java types. It can
only be used in annotations. It is equivalent to
The following is the syntax of class initializers.
class-initializer-decl ::= [ method-specification ] [
The first form above is the form of Java class instance and static
initializers. The initializer is static, and thus run when the class
is loaded, if it is labeled
static. The effect of the
initializer can be specified by a JML method specification
(see section 9. Method Specifications), which
treats the initializer as a private helper method with return type
void, whose body is given by the compound-statement
(see section 12. Statements and Annotation Statements).
The last two forms are used in JML to specify static and
instance initializers without giving the body of the initializer.
They would be used in annotations in non-Java files
(see section 16. Refinement). At most one of each of these may appear in a type
specification file. Such a specification is satisfied if there is at
least one corresponding initializer in the implementation, and if
the sequential composition of the bodies of the corresponding
initializer(s), when considered as the body of a private helper method
with return type
void, satisfy the specification given
(see section 9. Method Specifications).
Note that, due to this semantics, the method-specifications for an initializer can only have private specification cases.
[[[ But initializers can be interspersed between field initializations, which will affect their meaning. Thus I think the composition has to include the field initializations. The effect is that the post-condition of the JML initializer refers to the state before a constructor begins executing; a static_initializer refers to the state after class loading, I think. -- DRCok ]]] [[[ Is the restriction to private true for static initialization as well - don't think it should be. - DRCOk ]]]
|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|