Go to the first, previous, next, last section, table of contents.

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

   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.

   Omitted clause (heavyweight) 
   continues      false
   breaks         false 
   returns        false

Go to the first, previous, next, last section, table of contents.