|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|
As noted above (see section 1.2 Lightweight Specifications),
specifications in JML do not need to be as detailed
as most of the examples given in this document.
If a spec-case
does not use one of the behavior keywords
or if an example
does not use one of the example keywords
then it is called a lightweight specification or example.
Otherwise it is a heavyweight specification or example.
When the various clauses of a spec-case
or example are omitted, they have
the defaults given in the table below. The table distinguishes between
lightweight and heavyweight specifications and examples. In most cases
the default for the lightweight form is that
no assumption is made about the omitted clause. There are only two
exceptions to this rule. The first is that for an omitted
diverges clause defaults to
false. The second is that
signals_only has a default that depends on the
exceptions declared in the method.
Default Omitted clause lightweight heavyweight ___________________________________________________________ requires \not_specified true diverges false false measured_by \not_specified \not_specified assignable \not_specified \everything when \not_specified true working_space \not_specified \not_specified duration \not_specified \not_specified ensures \not_specified true signals_only see text see text signals \not_specified (Exception) true
However, in a heavyweight
specification or example, the specifier is assumed to be giving a complete
specification or example. Therefore, in a heavyweight specification the
meaning of an omitted clause is given a definite default.
For example, the meaning of an omitted
is that all locations (that can otherwise be legally assigned to)
can be assigned.
Furthermore, in a non-lightweight specification, the meaning of an
omitted diverges clause is that the method may not diverge in that case.
diverges clause is almost always omitted; it can be used
to say what should be true, of the pre-state, when the specification
is allowed to loop forever or signal an error.)
The defaults for omitted
signals clauses do
not apply to
normal_behavior specification cases, since
normal_behavior specification cases cannot contain these clauses.
The default for the
signals_only clause is the same in both
heavyweight and lightweight specifications, but depends on the list of
exceptions declared in the method. If the method declares no
exceptions, then the default clause is
(which means that the method cannot throw any exceptions).
However, if the method header declares that the method may throw
exceptions DE1, ..., DEn, then the default
signals_only clause is as follows.
signals_only DE1, ..., DEn
signals_onlyclause is omitted from a specification case, even if the method has a
signalsclause. If this default is too strong, the effect can be changed by either writing an explicit
signals_onlyclause, or by declaring further exceptions in the method's header. Note that although Java allows runtime exceptions (subtypes of
java.lang.RuntimeException) to be thrown without being declared in a method's header, JML does not take make a special case for these.
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
pure that add implicit
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
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
also; it is used so as not to
change the meaning of the inherited specification.
If the code is annotated with keywords like
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.
It is intended that the meaning of
\not_specified may vary
between different uses of a JML specification.
For example, a static checker might treat a
\not_specified as if it were
while a verification logic might treat it as if it were
However, a reasonable default for the interpretation for
in a lightweight specification is the most liberal possible
(i.e., the one that permits the most correct implementations); this is
generally the same as the heavyweight default, except for the
diverges clause (where the most liberal interpretation would be
Note that specification statements (see the JML Reference manual [Leavens-etal-JMLRef] for details) cannot be lightweight. In addition, a spec-statement can specify abrupt termination. The additional clauses possible in a spec-statement have the following defaults. These are not liberally interpreted, but instead prohibit the statement from having abrupt behavior by default.
Default Omitted clause (heavyweight) ____________________________ continues false breaks false returns false
|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|