A. Specification Case Defaults

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 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 an omitted 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 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.)

The defaults for omitted signals_only and 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 signals_only \nothing; (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

This default applies whenever the signals_only clause is omitted from a specification case, even if the method has a signals clause. If this default is too strong, the effect can be changed by either writing an explicit signals_only clause, 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 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.

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 \not_specified 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 true).

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