|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|
JML has several features that allow the specification of implications [Tan95] and examples [Leavens97c] [Leavens-Baker99]. They are redundant in the sense that they do not constrain an implementation directly. Instead, they are useful for pointing out consequences to the specification's readers, for example to draw attention to some consequences of the specification of a method, or to illustrate it by an example.
In addition to clauses of the form X
_redundantly, such as
ensures_redundantly, etc., there
are two sections of a method specification that are devoted to such
These sections of a method specification are described by the
redundant-spec ::= implications [ examples ] | examples
The two subsections below explain these features. The description of
clauses of the form X
_redundantly is contained in the first
A redudant implication is a way of stating a claim about a specification. By itself it does not constrain an implication, but can be thought of a stating a theorem to be proven about a specification. Such redundant implications are useful for drawing the reader's attention to some point that might otherwise be overlooked, or that is important for rhetorical purposes [Leavens-Baker99].
Redundant implications can be specified in two ways in JML.
The first is by using clauses of the form
The second is by use of the implications section of a method
specification, which starts with the keyword
(See section 9.2 Organization of Method Specifications, for the syntax of
The implications section of a method specification says that for each visibility level V, and for each spec-case of visibility V in its spec-case-seq, that spec-case is refined by the entire non-redundant specification of the method that applies at visibility level V. Thus every correct implementation of the non-redundant specification must satisfy each of the spec-cases in the implications section.
For example, suppose that the (desugared) meaning of the non-redundant part of a method's specification has the form:
V behavior // non-redundant requires Pre; assignable x1, x2; ensures NormPost; signals_only Ex1; signals (Exception e) ExPost;
and suppose that one of the spec-cases in its implications section has the following (desugared) meaning:
V behavior // redundant requires RedPre; assignable x1, x2; ensures RedNormPost; signals_only Ex1; signals (Exception e) RedExPost;
Then it must be the case that (by definition of refinement for method specifications [Leavens-Naumann06]) the following implications hold:
\old(RedPre) ==> Pre,
(\old(RedPre) && NormPost) ==> RedNormPost, and
(\old(RedPre) && ExPost) ==> RedExPost.
These implications are only sensible if the
specifications have the same visibility (
and the same
assignable clauses differ, one can adjust by adding elements to
the non-redundant parts of the assignable clause, to widen it,
but preserve its meaning by adding restrictions
(e.g., using the
\only_assigned predicate), to the postconditions.
Similar adjustments can be made to the non-redundant
signals_only clause, by adding exceptions (or supertypes of
exceptions) to the non-redundant
preserving its meaning by adding restrictions in the
Redundant clauses are a syntactic variant of Tan's procedure claims
The meaning of a redundant clause,
of the form X
_redundantly is also defined as making a claim
about implications, but in this case only one simple implication.
The claim is that the predicate in the redundant clause follows from
the meaning of the non-redundant X clauses.
As an example, consider the following requires clauses.
requires Pre; requires_redundantly RedPre;
These state the claim that
Pre ==> RedPre.
That is, in all pre-states, whenever
Pre is true, then
RedPre must be true.
The same pattern holds for all other clauses and their redundant
counterparts, including ensures clauses, signals clauses (which must
first be standardized to have the same exception
[Raghavan-Leavens05]), invariants, etc.
For example, recall that multiple clauses are conjoined, and thus
ensures Q1; ensures Q2; ensures_redundantly RedQ1; ensures_redundantly RedQ2;
is equivalent to
ensures Q1 && Q2; ensures_redundantly RedQ1 && RedQ2;
In this example, the claim stated is that:
(Q1 && Q2) ==> (RedQ1 && RedQ2).
If one is using a theorem prover, then these implications can be thought of as theorems to prove (in the context of the overall class or interface specification).
A runtime assertion checker is free to check the specifications in the implications section, since they must all hold, as they should be refined by the non-redundant specification. If a redundant specification case in a method's implications section is violated, this could indicate that either: (a) the implications described above do not hold, or that (b) there is a violation of the specification by the caller (e.g., if the precondition does not hold) or by the implementation of the method (e.g., if the normal postcondition does not hold).
[[[Needs concrete examples.]]]
Examples are, used to point out, to readers or testing tools,
particular cases of a method specification [Leavens97c]
The following gives the syntax of the examples section of a
This section starts with the
for_example keyword, and includes
one or more examples.
Each example is much like a spec-case
(see section 9.2 Organization of Method Specifications),
but uses various
example keywords instead of
keywords, and does not permit model-program cases.
As in method spec-cases
(see section 9.2 Organization of Method Specifications)
there are both heavyweight and lightweight examples.
A lightweight example does not use one of the
A heavyweight example uses one of the example keywords.
As with spec-cases, only heavyweight examples can have a
specified visibility; lightweight examples all have the same
visibility as the method (or constructor) being specified.
The defaults for omitted clauses in lightweight examples are the same as those for omitted clauses in lightweight spec-cases. Similarly, heavyweight examples have the same defaults as heavyweight spec-cases. (See section 9.6.1 Semantics of flat behavior specification cases, for the defaults for a lightweight and heavyweight specification cases.)
As described in the "Preliminary Design of JML" [Leavens-Baker-Ruby06] (section 220.127.116.11) "the specification in each example should be such that:
public normal_behavior" specification case "and if there are no preconditions and assignable clauses, then the example's postcondition should the equivalent to the conjunction of the example's precondition and the postcondition of the
[[[(Needs concrete examples :-)]]]
|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|