| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The nonterminal field describes all the members of classes and interfaces (see section 6.1 Class and Interface Declarations).
field ::= member-decl
| jml-declaration
| class-initializer-decl
| |
Also see section G.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.
7.1 Java Member Declarations 7.2 Class Initializer Declarations
The following gives the syntax of Java member declarations.
member-decl ::= method-decl
| variable-definition
| class-declaration
| interface-declaration
|
See section 6.1 Class and Interface Declarations, for details of class-declaration and interface-declaration. We discuss method and variable declarations below.
7.1.1 Method and Constructor Declarations 7.1.2 Field and Variable Declarations
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 15.2 Extracting Model Program Specifications, for an explanation of
this modifier.
7.1.1.1 Formal Parameters 7.1.1.2 Model Methods and Constructors 7.1.1.3 Pure Methods and Constructors 7.1.1.4 Helper Methods and Constructors
formals ::= |
See section 7.1.2.2 Type-Specs, for more about the nonterminals type-spec and dims.
The modifier 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
[Raghavan-Leavens05].
The 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.
The non_null modifier may be added to a method in a separate
file (see section 17. Separate Files for Specifications),
and thus need not appear originally in the Java source code.
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 (although there is no particular purpose served by making a constructor final, since constructors are not overridden in any case).
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 15. 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
declared as pure.
This subsubsection, which describes the effect of the pure modifier
on methods and constructor declarations, is quoted from the preliminary design
document [Leavens-Baker-Ruby06].
We say a method
is pure if it is either specified with
the modifier 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
the modifier pure or appears in the specification of a pure
class.
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 theorem provers by making pure methods more like mathematical functions.
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
pure methods.
When recursion is used in a specification,
the proof of well-formedness for the specification
involves the use of JML's measured_by clause.
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 pure.
Note that this does not mean that all methods inherited (but not
declared in and hence not overridden in) the class or interface are
pure.
For example, every class inherits ultimately from
java.lang.Object,
which has some methods, such as notify and notifyAll
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
with the pure modifier as pure.
In JML the modifiers model and pure
are orthogonal. (Recall something declared with
the modifier 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
with void as their return type are not illegal, they are
useless.
The helper modifier may only be used on a private method or
constructor [Leavens-Mueller07].
See section 6.2.9 Helper, for more on why such methods and constructors
must be private.
A method or constructor with the helper modifier,
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 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 ::= [ |
The 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
the keyword 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 `.jml'
(see section 17. Separate Files for Specifications), 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 12.2 Specification Expressions, for the syntax of expression. In the following we discuss the modifiers for field and variable declarations and type-specs.
7.1.2.1 JML Modifiers for Fields 7.1.2.2 Type-Specs
The ghost and 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 13. 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
JML.
While fields can be declared as either model or ghost fields, a field
cannot be both. Furthermore, local variables cannot be declared with
the model modifier.
The 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
invariants.
The 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
[Leino-Nelson-Saxe00].
It may not be used with model fields.
The 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
used explicitly).
See section 2.5 Instance vs. Static.
To declare a static field in an interface, one omits the
instance modifier; such a field, as in Java is both static and final.
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 ]
| |
The type \TYPE represents the kind of all Java types. It can
only be used in annotations. It is equivalent to
java.lang.Class.
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 13. 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 17. Separate Files for Specifications). 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] | [ ? ] |