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
(behavior, normal_behavior, or exceptional_behavior),
or if an example
does not use one of the example keywords
(example, normal_example,
exceptional_example),
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 each case
the default for the lightweight form is that
no assumption is made about the omitted clause. 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 assignable clause
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.
(The 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.)
Default
Omitted clause lightweight heavyweight
___________________________________________________________
requires \not_specified true
diverges \not_specified 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 (Exception) \not_specified (Exception) true
A completely omitted specification is taken to be a lightweight specification. Thus one can read off the meaning of a completely omitted specification from the lightweight column of table.
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 requires clause
that is \not_specified as if it were true,
while a verification logic might treat it as if it were false.
However, a reasonable default for the interpretation for an omitted
clause 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.
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.
Default
Omitted clause (heavyweight)
____________________________
continues false
breaks false
returns false
Go to the first, previous, next, last section, table of contents.