14. Redundancy

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 requires_redundantly, ensures_redundantly, etc., there are two sections of a method specification that are devoted to such redundant specifications. These sections of a method specification are described by the following grammar.

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

14.1 Redundant Implications and Redundantly Clauses
14.2 Redundant Examples

14.1 Redundant Implications and Redundantly Clauses

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 X_redundantly. The second is by use of the implications section of a method specification, which starts with the keyword implies_that. (See section 9.2 Organization of Method Specifications, for the syntax of spec-case-seq.)

implications ::= implies_that spec-case-seq

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 (V), the same assignable clauses, and the same signals_only clauses. If the 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 signals_only, preserving its meaning by adding restrictions in the signals clause.

Redundant clauses are a syntactic variant of Tan's procedure claims [Tan95]. 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.]]]

14.2 Redundant Examples

Examples are, used to point out, to readers or testing tools, particular cases of a method specification [Leavens97c] [Leavens-Baker99] [Leavens-Baker-Ruby06]. The following gives the syntax of the examples section of a method specification. 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 behavior keywords, and does not permit model-program cases.

examples ::= for_example example [ also example ] ... example ::= [ [ privacy ] example ] [ spec-var-decls ] [ spec-header ] simple-spec-body | [ privacy ] exceptional_example [ spec-var-decls ] spec-header [ exceptional-example-body ] | [ privacy ] exceptional_example [ spec-var-decls ] exceptional-example-body | [ privacy ] normal_example [ spec-var-decls ] spec-header [ normal-example-body ] | [ privacy ] normal_example [ spec-var-decls ] normal-example-body exceptional-example-body ::= exceptional-spec-case [ exceptional-spec-case ] ... normal-example-body ::= normal-spec-case [ normal-spec-case ] ...

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 example keywords. 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 2.3.2.1) "the specification in each example should be such that:

• the example's precondition implies the precondition of the expanded meaning of the specified behaviors,

• the example's assignable clause specifies a subset of the locations that are assignable according to the expanded meaning of the specified behaviors, and

• assuming the example's assignable clause, the conjunction of:
  • the example's precondition (wrapped by \old()),

  • the precondition of the expanded meaning of the specified behaviors (also wrapped by \old()), and

  • the postcondition of the expanded meaning of the specified behaviors
  should be equivalent to the example's postcondition.

[[[(Needs concrete examples :-)]]]