| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Although the use of pre- and postconditions for specification of the
behavior of methods is standard, JML offers some features that are
not so standard. A good example of such a feature is the distinction
between normal and exceptional postconditions (in ensures and
signals clauses, respectively), and the specification of frame
conditions using assignable clauses. Another example of such a
feature is that JML uses privacy modifiers to allow one to write
different specification that are intended for different readers; for
example, one can write a public specification for clients, a protected
specification for subclasses, and a private specification to record
implementation design decisions.
Yet another such feature is the use of redundancy to allow one to
point out important consequences of a specification for readers
[Tan95] [Leavens-Baker99].
JML provides two constructs for specifying methods and constructors:
This chapter only discusses the first of these, which is by far the most common. Model programs are discussed in 15. Model Programs.
[[[Discuss the "client viewpoint" here and give some basic examples here.]]]
[[[Perhaps discuss other common things to avoid repeating ourselves below...]]]
The following gives the syntax of behavioral specifications for methods. We start with the top-level syntax that organizes these specifications.
method-specification ::= specification | extending-specification extending-specification ::= |
Redundant specifications (redundant-spec) are discussed in 14. Redundancy.
A
method-specification of a method in a class or interface must start with
the keyword also if (and only if)
this method is already declared in the parent
type that the current type extends, in one of the interfaces the class
implements, or in a previous file of the refinement sequence for this type.
Starting a method-specification with the keyword also is
intended to tell the reader that this specification is in addition to
some specifications of the method that are given in the superclass of
the class, one of the interfaces it implements, or in another file in the
refinement sequence.
A method-specification can include any number of
spec-cases, joined by the keyword also,
as well as a redundant-spec.
Aside from the redundant-spec, each of the spec-cases
specifies a behavior that must be satisfied by
a correct implementation of the method or constructor.
That is, whenever a call to the specified method or constructor satisfies
the precondition of one of its spec-cases,
the rest of the clauses in that spec-case
must also be satisfied by the implementation
[Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b]
[Raghavan-Leavens05] [Wills92b] [Wing83].
Model program specification cases, which have no explicit
preconditions, must be satisfied by all implementations.
The spec-cases in a method-specification can have several forms:
spec-case ::= lightweight-spec-case | heavyweight-spec-case
| model-program
|
Model programs are discussed in 15. Model Programs. The remainder of this chapter concentrates on lightweight and heavyweight behavior specification cases. JML distinguishes between
behavior, normal_behavior or
exceptional_behavior, or one of their British variant spellings
keywords behaviour, normal_behaviour or
exceptional_behaviour
(these are also called behavior, normal
behavior, and exceptional behavior specification cases, respectively),
and
A lightweight specification case is similar to a behavior specification case, but with different defaults [Leavens-Baker-Ruby06]. It also is possible to desugar all such specification cases into behavior specification cases [Raghavan-Leavens05].
Heavyweight specification cases may be declared with an explicit access modifier, according to the following syntax.
privacy ::= |
The access modifier of a heavyweight specification case
cannot allow more access than the method being specified.
So a public method may have a private behavior specification,
but a private method may not have a public public specification.
A heavyweight specification case without an explicit access modifier
is considered to have default (package) access.
Lightweight specification cases have no way to explicitly specify an
access modifier, so their access modifier is implicitly the same
as the method being specified. For example, a lightweight specification
of a public method has public access, implicitly,
but a lightweight specification
of a private method has private access, implicitly.
Note that this is a different default than that for heavyweight
specifications, where an omitted access modifier always means package access.
The access modifier of a specification case affects only which annotations are visible in the specification and does not affect the semantics of a specification case in any other way.
JML's usual visibility rules apply to specification cases. So, for example, a public specification case may only refer to public members, a protected specification case may refer to both public and protected members, as long as the protected members are otherwise accessible according to Java's rules, etc. See section 2.4 Privacy Modifiers and Visibility, for more details and examples.
The following is the syntax of lightweight specification cases. These are the most concise specification cases.
lightweight-spec-case ::= generic-spec-case
generic-spec-case ::= [ spec-var-decls ]
spec-header
[ generic-spec-body ]
| [ spec-var-decls ]
generic-spec-body
generic-spec-body ::= simple-spec-body
| |
As far as the syntax is concerned, the only difference between a
lightweight specification case and a behavior-specification-case
(see section 9.6 Behavior Specification Cases) is that the latter has the
keyword behavior and possibly an access control modifier.
A lightweight specification case always has the same access modifier as the method being specified, see 9.3 Access Control in Specification Cases. To specify a different access control modifier, one must use a heavyweight specification.
A lightweight specification case can be understood as syntactic sugar for
a behavior specification case,
except that the defaults for omitted
specification clauses are different for lightweight specification cases
than for behavior specification cases.
So, for example, apart from the class names,
method m in class Lightweight below
package org.jmlspecs.samples.jmlrefman;
public abstract class Lightweight {
protected boolean P, Q, R;
protected int X;
/*@ requires P;
@ assignable X;
@ ensures Q;
@ signals (Exception) R;
@*/
protected abstract int m() throws Exception;
}
|
m in class Heavyweight below.
package org.jmlspecs.samples.jmlrefman;
public abstract class Heavyweight {
protected boolean P, Q, R;
protected int X;
/*@ protected behavior
@ requires P;
@ diverges false;
@ assignable X;
@ when \not_specified;
@ working_space \not_specified;
@ duration \not_specified;
@ ensures Q;
@ signals_only Exception;
@ signals (Exception) R;
@*/
protected abstract int m() throws Exception;
}
|
As this example illustrates, the default for an omitted clause in a
lightweight specification is \not_specified for all clauses,
except diverges, which has a default of false, and
signals [Leavens-Baker-Ruby06]. The default for an omitted
signals clause is to only permit the exceptions declared in the
method's header to be thrown. Thus, if the method declares that
exceptions DE1 and DE2 may be thrown, then the default
for an omitted signals clause is
signals (Exception e) e instanceof DE1 || e instanceof DE2; |
\not_specified may vary between different uses of a JML
specification. For example, a static checker might treat a
requires clause that is \not_specified as if it were
true, while a verification logic may decide to treat it as if it
were false.
A completely omitted specification is taken to be a lightweight specification. If the default (zero-argument) constructor of a class is omitted because its code is omitted, then its specification defaults to an assignable clause that allows all the locations that the default (zero-argument) constructor of its superclass assigns -- in essence a copy of the superclass's default constructor's assignable clause. If some other frame is desired, then one has to write the specification, or at least the code, explicitly.
A method or constructor with code present has a
completely omitted specification if it has no
specification-cases and does not use
annotations like non_null or pure that add implicit
specifications.
If a method or constructor has code, has a completely omitted
specification, and does not override another method, then
its meaning is taken as the lightweight specification
diverges \not_specified;.
Thus, its meaning can be read
from the lightweight column of table above, except that the diverges
clause is not given its usual default.
This is done so that the default
specification when no specification is given truly says nothing about
the method's behavior.
However, if a method with code and a completely omitted
specification overrides some other method, then its meaning is taken
to be the lightweight specification also requires false;. This somewhat
counter-intuitive specification is the unit under specification
conjunction with also; it is used so as not to
change the meaning of the inherited specification.
If the code is annotated with keywords like non_null or
pure that add implicit specifications, then these implicit
specifications are used instead of the default. Code with such
annotations is considered to have an implicit specification.
There are three kinds of heavyweight specification cases, called
behavior, normal behavior, and exceptional behavior specification
cases, beginning (after an optional privacy modifier) with the one of
the keywords behavior, normal_behavior, or
exceptional_behavior, respectively.
heavyweight-spec-case ::= behavior-spec-case
| exceptional-behavior-spec-case
| normal-behavior-spec-case
|
Like lightweight specification cases, normal behavior and exceptional
behavior specification cases can be understood as syntactic sugar for
special kinds of behavior specification cases
[Raghavan-Leavens05].
The behavior specification case is the most general form of
specification case. All other forms of specification cases simply
provide some syntactic sugar for special kinds of behavior
specification cases.
As far as the syntax is concerned, the only difference between a
behavior specification case and a lightweight one is
the optional access control modifier, privacy,
and the keyword behavior (or the British variant, behaviour).
One can use either the British or the American spelling of this
keyword, although for historical reasons most examples will use the
American spelling.
behavior-spec-case ::= [ privacy ] [ |
See section 16.2 Code Contracts, for details of the semantics of
behavior-spec-cases that use the code keyword.
To explain the semantics of a behavior specification case we make a distinction between flat and nested specification cases:
|
require, ensures, etc. clauses,
and its semantics is explained directly in
9.6.1 Semantics of flat behavior specification cases.
{| and |} to nest
specification clauses and possibly also also inside these
brackets to join several specification cases.
A nested specification case can be syntactically desugared into a list
of one or more simple specification cases, joined by the also
keyword [Raghavan-Leavens05].
This is explained in 9.6.5 Semantics of nested behavior specification cases.
The semantics of a behavior specification case for a method or constructor in a class depends on the invariants and constraints that have been specified. This is discussed in 8.2 Invariants and 8.3 Constraints. In a nutshell, methods must preserve invariants and respect constraints, and constructors must establish invariants.
Below we explain the semantics of a simple behavior-spec-case
case with precisely
one requires clause,
one diverges clause,
one measured_by clause,
one assignable clause,
one accessible clause,
one callable clause,
one when clause,
one ensures clause,
one duration clause,
one working_space clause,
one signals_only clause,
and
one signals clause.
A behavior specification case can contain any number of these
clauses, and there are defaults that allow any of them to be omitted.
However, as explained in 9.9 Method Specification Clauses, any
behavior specification case is equivalent with a behavior
specification case of this form.
Consider a non-helper instance method m, and a
specification case of the following form.
behavior
forall T1 x1; ... forall Tn xn;
old U1 y1 = F1; ... old Uk yk = Fk;
requires P;
measured_by Mbe |
The meaning of this specification case is as follows.
Consider a particular call of the method m.
The state of the program after passing parameters to m, but before running any of the code of m is called the pre-state of the method call.
Suppose all applicable invariants hold in the pre-state of this call.
For every possible value of the variables declared in the
forall clauses, x1, ..., xn, the following must be
true. (If there are no forall clauses, then the following just
has to hold all by itself.)
Suppose that the variable y1 is bound to the pre-state value of
F1 in the pre-state (i.e., the beginning of the method, after
parameter passing), and in turn each of the old variable
declarations are bound to the values of the corresponding expressions,
also evaluated in the pre-state, and finally yk is bound to the value
of Fk in the pre-state. These bindings can depend on previously
defined old variable declarations in the specification case.
(If there are no old clauses, then no such variables are
bound.)
We call the state with such bindings in place the augmented pre-state.
Suppose also that with these binding
(i.e., in the augmented pre-state), that the precondition, P, from
the requires clause, holds.
If the method has a measured_by clause,
and if the predicate in the measured_by clause,
Mbp, is true in the augmented pre-state,
and if this call is in the control flow of another instance of this
method, Caller,
then the value of the expression Mbe in this call's augmented pre-state
must be non-negative and strictly less than the value of
Mbe in the pre-state of Caller.
(If the measured_by clause is omitted, there is no such requirement.)
For example, consider a method fib that calls itself directly
and has an integer parameter n and for which the
measured_by clause has n as its expression (Mbe),
and the default predicate (Mbp) is true;
then recursive calls of fib that appear in the body of
fib must have actual argument exprssions whose value is
(non-negative and)
strictly less than n, such as n-1 and n-2.(8)
Then one of the following must also hold:
diverges predicate, D, holds in the augmented pre-state
and the execution of the method does not terminate (i.e., it loops
forever or the Java virtual machine exits in such a way that the method call
does not return or throw an exception). (If the diverges clause
is omitted, then the default for D is false, and hence
these outcomes are effectively prohibited.)
or
java.lang.Throwable whose type does not inherit from
java.lang.Exception, usually an instance of java.lang.Error), or
commit" [Rogriguez-etal05]) in a state such
that the when clause's condition, W, holds.
(If the condition does not hold,
then the method's execution waits for a concurrent thread to make it
true, and then proceeds. There is no guarantee that the method will
proceed the first time this condition holds, so the condition may have
to hold many times before the thread may proceed to its commit point.)
(If the when clause is omitted, there is no need to have a
commit point in the method, and the method need not wait for the
execution of concurrent threads.)
accessible and assignable clauses
or that are dependees (see section 10. Data Groups) of such locations,
are read from.
The set of locations named by the accessible and assignable clauses
(and hence the elements of their data groups) are computed in the pre-state.
(If the accessible clause is omitted, it defaults to
accessible \everything;, which allows all locations to be accessed.)
assignable clause's list, A,
or are dependees (see section 10. Data Groups) of such locations,
are assigned to.
The set of locations named by the assignable clause (and hence the
elements of their data groups) are computed in the pre-state.
(If the assignable clause is omitted, it defaults to
assignable \everything;, which allows all locations to be assigned.)
callable clause's list p1, ..., pl.
(If the callable clause is omitted, it defaults to
callable \everything;, which allows all methods and
constructors to be called.)
The form p.* refers to all methods of the object denoted by p.
captures clause's list, Z, may be assigned to fields of
some object or to array elements.
(References in formals may freely be assigned to local variables,
however, as these are "borrowed" but not captured [Boyland00].
If the captures clause is omitted, then all such formals may
be assigned freely.)
ensures
clause, holds in the post-state.
java.lang.Exception, then:
signals_only clause (this list
of types has as its default the list in the method's throws
clause), and
signals
clause, then the exceptional postcondition R must hold in the
post-state, augmented by a binding from the variable e to
the exception object thrown.
working_space clause,
Wsp, was true in the augmented pre-state, then
the method execution had available to it the amount of heap space, in bytes,
Wse [Krone-Ogden-Sitaraman03].
(Note that the expression Wse may depend on post-state values
so this expression is conceptually evaluated in the post-state,
although it may use \old() to refer to pre-state values.
If the working_space clause is omitted, there is no restriction
placed on the maximum space that the method call may during its execution.)
duration clause,
Dp, was true in the augmented pre-state, then
the method execution used no more than the number of virtual machine
cycles given by the expression De [Krone-Ogden-Sitaraman03].
(Note that the expression De may depend on post-state values
so this expression is conceptually evaluated in the post-state,
although it may use \old() to refer to pre-state values.
If the duration clause is omitted, there is no restriction
placed on the maximum number of virtual machine cycles that the call
may use during its execution.)
In all of these clauses, the value of a formal parameter is always considered to be the value they had in the pre-state. That is the actual post-state value they take in an execution is not considered, as explained in See section 9.9.6 Parameters in Postconditions.
The semantics of a flat specification case for a (non-helper)
constructor is the same as that for a (non-helper) method given
above, except that:
The semantics of a flat specification case for a helper method (or constructor) is the same as that for a non-helper method (or constructor) given above, except that:
We now explain how all behavior specification cases can be desugared
into a list of one or more flat specification cases joined by the
also keyword [Raghavan-Leavens05]. The semantics of a behavior
specification case is then simply the semantics of this desugared
version.
The desugaring is as follows. Consider a specification of the form.
spec-var-decls
spec-header
{|
GenSpecCase1
also
...
also
GenSpecCasen
|}
|
The above desugars to the following.
spec-var-decls
spec-header
GenSpecCase1
also
...
also
spec-var-decls
spec-header
GenSpecCasen
|
In the above desugaring either the spec-var-decls or the spec-header (or both) may be omitted.
The meaning of the desugared list of specification cases is explained in 9.2 Organization of Method Specifications. The meaning of a single simple specification case is explained in 9.6.1 Semantics of flat behavior specification cases.
A normal_behavior specification case is just syntactic sugar for
a behavior specification case with an implicit signals
clause
signals (java.lang.Exception) false; |
RuntimeException is a subclass of Exception.
The following gives the syntax of the body of a normal behavior specification case.
normal-behavior-spec-case ::= [ privacy ] [ |
As far as syntax is concerned, the only difference between a normal-spec-case and a generic-spec-case is that normal behavior specification cases cannot include signals-clauses or signals-only-clauses.
The semantics of a normal behavior specification case is the same as the
corresponding
behavior specification case
(see section 9.6 Behavior Specification Cases)
with the addition of the following
signals-clause
signals (java.lang.Exception) false; |
So a normal behavior specification case specifies a precondition which guarantees normal termination; i.e., it prohibits the method from throwing an exception.
The following gives the syntax of the body of an exceptional behavior specification case.
exceptional-behavior-spec-case ::= [ privacy ] [ |
As far as syntax is concerned, the only difference between an exceptional-spec-case and a generic-spec-case is that exceptional behavior specification cases cannot include ensures-clauses.
The semantics of an exceptional behavior specification case is the same
as the corresponding behavior specification case
(see section 9.6 Behavior Specification Cases)
with the addition of the following
ensures clause.
ensures false; |
So an exceptional behavior specification case specifies a precondition which guarantees that the method throws an exception, if it terminates, i.e., a precondition which prohibits the method from terminating normally.
9.8.1 Pragmatics of Exceptional Behavior Specifications Cases
Note that an exceptional behavior specification case says that some
exception must be thrown if its precondition is met (assuming
the diverges clause predicate is false, as is the default.)
Beware of the difference between specifying that an exception
must be thrown and specifying that an exception may be
thrown. To specify that an exception may be thrown you should
not use an exceptional behavior, but should instead use a
behavior specification case [Leavens-Baker-Ruby06].
For example, the following method specification
package org.jmlspecs.samples.jmlrefman;
public abstract class InconsistentMethodSpec {
/** A specification that can't be satisfied. */
/*@ public normal_behavior
@ requires z <= 99;
@ assignable \nothing;
@ ensures \result > z;
@ also
@ public exceptional_behavior
@ requires z < 0;
@ assignable \nothing;
@ signals (IllegalArgumentException) true;
@*/
public abstract int cantBeSatisfied(int z)
throws IllegalArgumentException;
}
|
z <= 99 and
z < 0 overlap, for example when z is -1. When
both preconditions hold then the exceptional behavior case specifies
that an exception must be thrown and the normal behavior case
specifies that an exception must not be thrown, but the
implementation cannot both throw and not throw an exception.
Similarly, multiple exceptional specification cases with overlapping preconditions may give rise to an inconsistent specification. For example, the following method specification
package org.jmlspecs.samples.jmlrefman;
public abstract class InconsistentMethodSpec2 {
/** A specification that can't be satisfied. */
/*@ public exceptional_behavior
@ requires z < 99;
@ assignable \nothing;
@ signals_only IllegalArgumentException;
@ also
@ public exceptional_behavior
@ requires z > 0;
@ assignable \nothing;
@ signals_only NullPointerException;
@*/
public abstract int cantBeSatisfied(int z)
throws IllegalArgumentException, NullPointerException;
}
|
signals_only clauses do not permit the same exception to be
thrown in both cases.
There is an important distinction to be made between the
signals and the signals_only clauses in JML.
The signals_only clause says what exceptions may be thrown
(when the specification case's precondition is met); this clause does
not say anything about the state of the exception object or other
locations in the system. On the other hand, the signals clause
only describes what must be true of the system state when an exception
is thrown, and does not say anything about what exceptions may be thrown.
For example, consider the following specification.
package org.jmlspecs.samples.jmlrefman;
public abstract class SignalsClause {
/*@ signals (IllegalArgumentException) x < 0;
@ signals (NullPointerException) x < 0;
@*/
public abstract int notPrecise(int x) throws RuntimeException;
}
|
IllegalArgumentException or
a NullPointerException when x is less than 0, but in
that condition the method might also throw a different exception
altogether, as long as that exception was permitted by the method's
declaration header. The only thing ruled out by this specification is
throwing either a IllegalArgumentException or
a NullPointerException when x is not less than 0.
Thus from such a specification one may draw the conclusion that
x < 0 only when one of these two exceptions is thrown.
Therefore, if one just wants to specify the exceptions that are permitted
to be thrown in a specific situation,
one should use the signals_only clause.
The different kinds of clauses that can be used in method specifications are discussed in this section. See section 9.4 Lightweight Specification Cases, for the overall syntax that ties these clauses together.
The syntax of spec-var-decls is as follows.
spec-var-decls ::= forall-var-decls [ old-var-decls ]
| old-var-decls
|
9.9.1.1 Forall Variable Declarations 9.9.1.2 Old Variable Declarations
The syntax of the forall-var-decls is as follows.
forall-var-decls ::= forall-var-declarator [ forall-var-declarator ] ... forall-var-declarator ::= |
When a forall-var-declarator is used, it specifies that the specification case that follows must hold for every possible value of the declared variables. In other words, it is a universal quantification over the specification case. See section 12.4.24 Quantified Expressions, for the syntax of quantified-var-declarator.
Note that if such variables are used in preconditions, then they can be thought to range over all values that satisfy the preconditions. The bound variable may not have the same name as earlier bound variables in the specification, nor may it shadow the formal parameters of the method declaration.
The syntax of the old-var-decls is as follows. See section 7.1.2.2 Type-Specs, for the syntax of type-spec. [[[Give cross ref for spec-variable-declarators when ready.]]]
old-var-decls ::= old-var-declarator [ old-var-declarator ] ... old-var-declarator ::= |
An old-var-declarator allows abbreviation within a specification case. The names defined in the spec-variable-declarators can be used throughout the specification case for the values of their initializers. As the name suggests, the expressions are evaluated in the method's pre-state. The bound variable may not rename earlier bound variables in the specification, nor the formal parameters of the method declaration.
[[[Example]]]
A requires clause specifies a precondition of method or constructor. Its syntax is as follows.
requires-clause ::= requires-keyword pred-or-not |
The predicate in a requires clause can
refer to any visible fields and to the parameters of the method.
See section 2.4 Privacy Modifiers and Visibility, for more details on visibility
in JML.
Any number of requires clauses can be included a single specification case. Multiple requires clauses in a specification case mean the same as a single requires clause whose precondition predicate is the conjunction of these precondition predicates in the given requires clauses. For example,
requires P; requires Q; |
requires P && Q; |
When a requires clause is omitted in a specification case,
a default requires clause is used.
For a lightweight specification case, the default precondition is
\not_specified.
The default precondition for a heavyweight specification case is
true.
At most one precondition in a specification case can use \same,
and \same cannot be used in the only specification case for a
method unless the method is an override (including overriding a
specification from an interface).
Similarly, \same cannot be used in the only specification case for a
constructor or a static method.
Another restriction is that \same cannot be used in a requires
clause of a nested specification case
(see section 9.6.5 Semantics of nested behavior specification cases).
When the precondition is \same in a specification case,
it means that the specification
case being written has, effectively, the same precondition as that
specified in the other (non-\same) specification cases.
That is, \same stands for
the disjunction (with ||) of the preconditions in all non-\same
specification cases of the method's specification from the current class
together with the inherited specification cases defined in its supertypes
(i.e., in its superclasses and implemented interfaces).
The order of this disjunction has, from left to right, inherited
preconditions before each of the preconditions from the specification
of any method that overrides it.
An ensures clause specifies a normal postcondition, i.e., a property that is guaranteed to hold at the end of the method (or constructor) invocation in the case that this method (or constructor) invocation returns without throwing an exception. The syntax is as follows See section 9.9.2 Requires Clauses, for the syntax of pred-or-not.
ensures-clause ::= ensures-keyword pred-or-not |
A predicate in an ensures clause can
refer to any visible fields, the parameters of the method,
\result if the method is non-void,
and may contain expressions of the form \old(E).
See section 2.4 Privacy Modifiers and Visibility, for more details on visibility
in JML.
Informally,
ensures Q; |
if the method invocation terminates normally (ie. without throwing an exception), then predicate Q holds in the post-state.
In an ensures clause,
\result stands for the result that is returned by the method.
The postcondition Q may contain expressions of
the form \old(e).
Such expressions are evaluated in the pre-state, and not in the post-state,
and allow Q to express a relation between the pre- and the post-state.
If parameters of the method occur in the postcondition Q,
these are always evaluated in the pre-state, not the post-state.
In other words, if a method parameter x occurs in Q,
it is treated as \old(x).
For a detailed explanation of this see 9.9.6 Parameters in Postconditions.
Any number of ensures clauses can be given in a single specification case. Multiple ensures clauses in a specification case mean the same as a single ensures clause whose postcondition predicate is the conjunction of the postcondition predicates in the given ensures clauses. So
ensures P; ensures Q; |
ensures P && Q; |
When an ensures clause is omitted in a specification case, a default
ensures clause is used. For a lightweight specification case, the
default precondition is \not_specified. The default
precondition for a heavyweight specification case is true.
In a specification case a signals clause specifies the
exceptional or abnormal postcondition, i.e., the property that is
guaranteed to hold at the end of a method (or constructor) invocation
when this method (or constructor) invocation terminates abruptly by
throwing a given exception.
The syntax is as follows. See section 9.9.2 Requires Clauses, for the syntax of pred-or-not.
signals-clause ::= signals-keyword |
In a signals-clause of the form
signals (E e) P; |
java.lang.Exception, and the
variable e is bound in P. If E is a checked exception
(i.e., if it does not inherit from java.lang.RuntimeException
[Arnold-Gosling-Holmes00] [Gosling-etal00]), it must either be one of
the exceptions listed in the method or constructor's throws
clause, or a subclass or a superclass of such a declared exception.
Informally,
signals (E e) P; |
If the method (or constructor) invocation terminates abruptly by throwing an exception of type E, then predicate P holds in the final state for this exception object E.
A signals clause of the form
signals (E e) R; |
signals (java.lang.Exception e) (e instanceof E) ==> R; |
Several signals clauses can be given in a single lightweight, behavior
or exceptional behavior specification case. Multiple signals clauses
in a specification case mean the same as a single signals clause whose
exceptional postcondition predicate is the conjunction of the
exceptional postcondition predicates in the given signals clauses.
This should be understood to take place after the desugaring given
above, which makes all the signals clauses refer to exceptions of type
java.lang.Exception. Also, the names in the given signals
clauses have to be standardized [Raghavan-Leavens05]. So for example,
signals (E1 e) R1; signals (E2 e) R2; |
signals (Exception e) ((e instanceof E1) ==> R1)
&& ((e instanceof E2) ==> R2);
|
[[[EXAMPLE]]]
Beware that a signals clause specifies when a certain exception
may be thrown, not when a certain exception must be
thrown. To say that an exception must be thrown in some situation,
one has to exclude that situation from other signals clauses and from
ensures clause (and any diverges clauses). It may also be useful to
use the signals_only clause in such specifications
(see section 9.9.5 Signals-Only Clauses).
[[[EXAMPLE?]]]
When a behavior or exceptional specification case has no
signals-clause, a default signals clause is used. For a
heavyweight specification case,
the default signals clause is signals (Exception) true;.
Since normal behavior specification cases do not have signals clauses,
no default applies for such specification cases.
For a lightweight specification case, the default is
signals \not_specified;.
A signals_only clause is an abbreviation for a
signals-clause (see section 9.9.4 Signals Clauses) that
specifies what exceptions may be thrown by a method, and thus, implicitly, what
exceptions may not be thrown.
The syntax is as follows.
signals-only-clause ::= signals-only-keyword reference-type [ |
All of the reference-types named in a signals-only-clause
must be subtypes of java.lang.Exception. Each
reference-type that is a checked exception type
(i.e., that does not inherit from java.lang.RuntimeException
[Arnold-Gosling-Holmes00] [Gosling-etal00]), must either be one of
the exceptions listed in the method or constructor's throws
clause, or a subclass or a superclass of such a declared exception.
A signals-only-clause of the form
signals_only E1, E2, ..., En; |
signals (java.lang.Exception e)
e instanceof E1
|| e instanceof E2
|| ...
|| e instanceof En;
|
Several signals-only-clauses can be given in a single
lightweight, behavior or exceptional behavior specification case.
Multiple such clauses
in a specification case mean the same as a single clause whose
list contains only the names Ej that are subtypes of some type
named in all of the given signals-only-clauses.
Thus, the meaning is a kind of intersection of the signals_only
clauses. Since this may be confusing, only one
signals_only clause should ever be used in a given specification case.
The signals_only clause is useful for specifying
when a certain exception, or one of a small set of exceptions, must be
thrown. To say that an exception must be thrown in some situation,
one has to exclude the method from returning normally in that
situation (using an ensures clause or the precondition of some other
specification case) and from not terminating (by using the diverges clause).
[[[Example]]]
If the signals_only is omitted from a specification case,
a default signals_only clause is provided.
The same default is used for both lightweight and heavyweight
behavior and exceptional behavior specification cases.
(Since normal behavior specification cases cannot throw exceptions at all,
there is no default signals_only clause for such specification cases.)
This default prohibits any exception not declared by the method in
the method's header from being thrown. Thus the exact default depends on the
method header. If the method header does not list any exceptions that
can be thrown, then the default is signals_only \nothing;
(which means that the method cannot throw any exceptions).
However, if the method header declares that the method may throw
exceptions DE_1, ..., DE_n, Err_1, ..., Err_m,
where each DE_i is a subtype of java.lang.Exception, and
each Err_j is not a subtype of java.lang.Exception,
then the default
signals_only clause is as follows.
signals_only DE_1, ..., DE_n |
public void foo() throws E1, E2 |
signals_only clause
would be
signals_only E1, E2; |
It is important to note that the set of exceptions included in the default
signals clause described above never includes
java.lang.Throwable, and does not include
java.lang.Error or any of its subtypes. Furthermore, this
default would not normally include
java.lang.RuntimeException or any of its subtypes, because Java
explicitly allows RuntimeExceptions to be thrown even if they are not
declared in the method header's throws clause.
Since such unchecked, runtime exceptions are not usually listed in the
method header, they would not find their way into the default
signals_only clause.
In JML, however, if you wish to allow such runtime exceptions, you
can either explicitly list them in the method header or, more
usually, you would list them in an explicit signals_only clause.
Parameters of methods are passed by value in Java, meaning that parameters are local variables in a method body, which are initialized when the method is called with the values of the parameters for the invocation.
This leads us to the following two rules:
\old() placed around
any occurrence of a formal parameter in a postcondition.
The justification for the first convention is that clients cannot observe assignments to the parameters anyway, as these are local variables that can only be used by the implementation of the method. Given that clients can never observe these assignments, there is no point in making them part of the contract between a class and its clients.
The justification for the second convention is that clients only know the initial values of the parameter that they supply, and do not have any knowledge of the final values that these variables may have in the post-state.
The reason for this is best illustrated by an example.
Consider the following class and its method specifications.
Without the convention described above
the implementations given for methods
notCorrect1 and notCorrect2 would satisfy their specifications.
However, clearly neither of these satisfies the specification
when read from the caller's point of view.
package org.jmlspecs.samples.jmlrefman;
public abstract class ImplicitOld {
/*@ ensures 0 <= \result && \result <= x;
@ signals (Exception) x < 0;
@*/
public static int notCorrect1(int x) throws Exception {
x = 5;
return 4;
}
/*@ ensures 0 <= \result && \result <= x;
@ signals (Exception) x < 0;
@*/
public static int notCorrect2(int x) throws Exception {
x = -1;
throw new Exception();
}
/*@ ensures 0 <= \result && \result <= x;
@ signals (Exception) x < 0;
@*/
public static int correct(int x) throws Exception {
if (x < 0) {
throw new Exception();
} else {
return 0;
}
}
}
|
The convention above rules out such
pathological implementations as notCorrect1
above; because mention of a formal parameter name, such as x above,
in postconditions always means the pre-state value of that name,
e.g., \old(x) in the example above.
The diverges clause is a seldom-used feature of JML. It can be used to specify when a method may either loop forever or not return normally to its caller. The syntax is as follows See section 9.9.2 Requires Clauses, for the syntax of pred-or-not.
diverges-clause ::= diverges-keyword pred-or-not |
When a diverges clause is omitted in a specification case, a default
diverges clause is used. For both lightweight and heavyweight
specification cases, the
default diverges condition is false.
Thus by default, specification cases
give total correctness specifications [Dijkstra76]. Explicitly writing
a diverges clause allows one to obtain a partial correctness
specification [Hoare69]. Being able to specify both total and partial
correctness specification cases for a method leads to additional power
[Hesselink92] [Nelson89].
As an example of the use of diverges, consider the abort
method in the following class. (This example is simplified from the
specification of Java's System.exit method.
This specification says that the method can always be called (the
implicit precondition is true),
may always not return to the caller (i.e., diverge),
and may never return normally, and
may never throw an exception.
Thus the only thing the method can legally do, aside from causing a JVM
error, is to not return to its caller.
package org.jmlspecs.samples.jmlrefman;
public abstract class Diverges {
/*@ public behavior
@ diverges true;
@ assignable \nothing;
@ ensures false;
@ signals (Exception) false;
@*/
public static void abort();
}
|
The diverges clause is also useful to specify things like methods that are supposed to abort the program when certain conditions occur, although that isn't really good practice in Java. In general, it is most useful for examples like the one given above, when you want to say when a method cannot return to its caller.
The when clause allows concurrency aspects of a method or
constructor to be specified [Lerner91] [Rodriguez-etal05].
A caller of a method will be delayed until the condition given in the
when clause holds. What is checked is that the method does not
proceed to its commit point, which is the start of execution of
statement with the label commit, until the given predicate is
true.
The syntax is as follows. See section 9.9.2 Requires Clauses, for the syntax of pred-or-not.
when-clause ::= when-keyword pred-or-not |
When a when clause is omitted in a specification case, a default when
clause is used. For a lightweight specification case, the default
when condition is \not_specified. The default when condition
for a heavyweight specification case is true.
See [Rodriguez-etal05] for more about the when clause and JML's
plans for support of multithreading.
An assignable clause gives a frame axiom for a specification. It says
that, from the client's point of view, only the locations named, and
locations in the data groups associated with these locations,
can be assigned to during the execution of the method.
The values of all subexpressions used in assignable clauses,
such as i-1 in a[i-1],
are computed in the pre-state of the method,
because the assignable clause only talks about locations that exist in
the pre-state.
See section 10. Data Groups, for more about specification of data groups. However, locations that are local to the method (or methods it calls) and locations that are created during the method's execution are not subject to this restriction.
The syntax is as follows. See section 12.7 Store Refs, for the syntax of store-ref-list.
assignable-clause ::= assignable-keyword store-ref-list |
When an assignable clause is omitted in a specification case, a
default assignable clause is used. This default has a default
store-ref-list. For a lightweight specification
case, the default store-ref-list is
\not_specified. The default store-ref-list
for a heavyweight specification case is \everything.
If one wants the opposite of the default (for a heavyweight specification case), then one can specify that a method cannot assign to any locations by writing:
assignable \nothing; |
pure on a method achieves the same effect as
specifying assignable \nothing, but does so for the method's entire
specification as opposed to a single specification-case.
Assignable clauses are subject to several restrictive rules in JML.
The first rule has to do with fields of model objects.
Because model objects are abstract
and do not have a concrete state or concrete fields, the JML typechecker
does not allow fields of model objects to be listed in the assignable clause;
that is, such expressions do not specify a set of locations
(concrete fields) that can be assigned to. Thus expressions
like f.x are not allowed in the assignable clause when f
is a model field.
[[[Flesh out other restrictions. Refer to [Mueller-Poetzsch-Heffter-Leavens03] for details.]]]
The accessible clause is a seldom-used feature of JML.
Together with the assignable clause (see section 9.9.9 Assignable Clauses),
it says what (pre-existing) locations a method may
read during its execution.
It has the following syntax.
accessible-clause ::= accessible-keyword store-ref-list |
During execution of the method (which includes all directly and
indirectly called methods and constructors),
only locations that either did not exist in the pre-state,
that are local to the method (including the method's formal parameters),
or that are either named in the lists found in the
accessible and assignable clauses
or that are dependees (see section 10. Data Groups) of such locations,
are read from.
Note that locations that are local to the method (or methods it calls)
and locations that are created during the method's execution are not
subject to this restriction and may be read from freely.
When an accessible clause is omitted in a code contract specification case, a
default accessible clause is used.
This default has a default store-ref-list which is
\everything.
See section 16. Specification for Subtypes, for more discussion and examples.
The callable clause says what methods may be called, either directly or indirectly, by the method being specified. It has the following syntax.
callable-clause ::= callable-keyword callable-methods-list |
During execution of a method,
the only methods and constructors that may be called are those listed in the
callable clause's list.
When a callable clause is omitted in a code contract specification case, a
default callable clause is used.
This default has a default callable-methods-list which is
\everything.
See section 16. Specification for Subtypes, for more discussion and examples.
A measured by clause can be used in a termination argument for a recursive specification. It has the following syntax.
measured-clause ::= measured-by-keyword |
The spec-expression in a measured by clause must have type
int.
In both lightweight and heavyweight specification cases, an omitted measured by clause means the same as a measured by clause of the following form.
measured_by \not_specified; |
The captures clause has the following syntax.
captures-clause ::= captures-keyword store-ref-list |
The captures clause says that references to the store-refs listed can be retained after the method returns, for example in a field of the receiver object or in a static field. Therefore, the captures clause specifies when an object, passed as an actual parameter in a method call, may be captured during the call.
An actual parameter object (including the receiver this) is captured if it appears on the right-hand side of an assignment statement during the call. This can also happen indirectly through another method or constructor call or by returning the parameter object as the method result (we assume the result will be assigned to a field or local variable after the call).
The captures clause is used to prevent certain kinds of representation exposure as part of an alias control technique. For example, if an object should not be aliased, then that object must not be passed to a method that may capture it, i.e., may create an alias to it (this includes the receiver). Furthermore, objects used as part of the abstract representation of a type should not be aliased, and thus should not be passed to methods that capture it. JML tools will eventually prevent such aliasing.
When a captures clause is omitted in a method specification case, then a
default captures clause is used.
This default has a default store-ref-list which is
\everything.
Thus when omitted, a method is allowed to capture any of the actual
parameter objects or the receiver.
A working-space-clause can be used to specify the maximum amount of heap space used by a method, over and above that used by its callers. The clause applies only to the particular specification case it is in, of course This is adapted from the work of Krone, Ogden, and Sitaraman on RESOLVE [Krone-Ogden-Sitaraman03].
working-space-clause ::= working-space-keyword |
The spec-expression in a working space clause must have type
long. It is to be understood in units of bytes.
The spec-expression in a working space clause may use
\old and other JML operators appropriate for postconditions.
This is because it is considered to be evaluated in the post-state,
and provides a guarantee of the maximum amount of additional space
used by the call. In some cases this space may depend on the
\result, exceptions thrown, or other post-state values.
[[[ There is however no way to identify the exception thrown - DRCok]]]
In both lightweight and heavyweight specification cases, an omitted working space clause means the same as a working space clause of the following form.
working_space \not_specified; |
See section 12.4.13 \working_space, for information about the
\working_space expression that can be used
to describe the working space needed by a
method call. See section 12.4.12 \space, for information about the
\space expression that can be used
to describe the heap space occupied by an object.
A duration clause can be used to specify the maximum (i.e., worst case) time needed to process a method call in a particular specification case. [[[ Tools are simpler if the argument can simply be an arbitrary expression rather than a method call. -- DRCok ]]] This is adapted from the work of Krone, Ogden, and Sitaraman on RESOLVE [Krone-Ogden-Sitaraman03].
duration-clause ::= duration-keyword |
The spec-expression in a duration clause must have type
long. It is to be understood in units of [[[the JVM
instruction that takes the least time to execute, which may be thought
of as the JVM's cycle time.]]] The time it takes the JVM to execute
such an instruction can be multiplied by the number of such cycles to
arrive at the clock time needed to execute the method in the given
specification case. [[[This time should also be understood as not
counting garbage collection time.]]]
The spec-expression in a duration clause may use
\old and other JML operators appropriate for postconditions.
This is because it is considered to be evaluated in the post-state,
and provides a guarantee of the maximum amount of additional space
used by the call. In some cases this space may depend on the
\result, exceptions thrown, or other post-state values.
[[[ There is no way to identify the exception thrown - DRCok]]]
In both lightweight and heavyweight specification cases, an omitted duration clause means the same as a duration clause of the following form.
duration \not_specified; |
See section 12.4.11 \duration, for information about the \duration
expression that can be used in the duration clause to specify the
duration of other methods.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |