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
(see section B.1.6 Behavioral Specification Syntax for Methods)
does not use one of the behavior keywords
or if an example (see section B.1.8 Example Syntax)
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 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
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.)
Default Omitted clause lightweight heavyweight ___________________________________________________________ requires \not_specified true when \not_specified true diverges \not_specified false working_space \not_specified \not_specified duration \not_specified \not_specified measured_by \not_specified \not_specified assignable \not_specified \everything 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
\not_specified as if it were
while a verification logic would need to treat it as if it were
Note that specification statements (see section B.1.7 Model Program Syntax) 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.