[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

9. Method Specifications

Although the use of pre- and postconditions for specification of the behavior of methods is standard, JML offers some features that are not so standard. A good example of such a feature is the distinction between normal and exceptional postconditions (in ensures and signals clauses, respectively), and the specification of frame conditions using assignable clauses. Another example of such a feature is that JML uses privacy modifiers to allow one to write different specification that are intended for different readers; for example, one can write a public specification for clients, a protected specification for subclasses, and a private specification to record implementation design decisions. Yet another such feature is the use of redundancy to allow one to point out important consequences of a specification for readers [Tan95] [Leavens-Baker99].

JML provides two constructs for specifying methods and constructors:

This chapter only discusses the first of these, which is by far the most common. Model programs are discussed in 15. Model Programs.

9.1 Basic Concepts in Method Specification  
9.2 Organization of Method Specifications  
9.3 Access Control in Specification Cases  
9.4 Lightweight Specification Cases  
9.5 Heavyweight Specification Cases  
9.6 Behavior Specification Cases  
9.7 Normal Behavior Specification Cases  
9.8 Exceptional Behavior Specification Cases  
9.9 Method Specification Clauses  


9.1 Basic Concepts in Method Specification

[[[Discuss the "client viewpoint" here and give some basic examples here.]]]

[[[Perhaps discuss other common things to avoid repeating ourselves below...]]]


9.2 Organization of Method Specifications

The following gives the syntax of behavioral specifications for methods. We start with the top-level syntax that organizes these specifications.

 
method-specification ::= specification | extending-specification
extending-specification ::= also specification
specification ::= spec-case-seq [ redundant-spec ]
              | redundant-spec
spec-case-seq ::= spec-case [ also spec-case ] ...

Redundant specifications (redundant-spec) are discussed in 14. Redundancy.

A method-specification of a method in a class or interface must start with the keyword also if (and only if) this method is already declared in the parent type that the current type extends, in one of the interfaces the class implements, or in a previous file of the refinement sequence for this type. Starting a method-specification with the keyword also is intended to tell the reader that this specification is in addition to some specifications of the method that are given in the superclass of the class, one of the interfaces it implements, or in another file in the refinement sequence.

A method-specification can include any number of spec-cases, joined by the keyword also, as well as a redundant-spec. Aside from the redundant-spec, each of the spec-cases specifies a behavior that must be satisfied by a correct implementation of the method or constructor. That is, whenever a call to the specified method or constructor satisfies the precondition of one of its spec-cases, the rest of the clauses in that spec-case must also be satisfied by the implementation [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b] [Raghavan-Leavens05] [Wills92b] [Wing83]. Model program specification cases, which have no explicit preconditions, must be satisfied by all implementations.

The spec-cases in a method-specification can have several forms:

 
spec-case ::= lightweight-spec-case | heavyweight-spec-case
        | model-program

Model programs are discussed in 15. Model Programs. The remainder of this chapter concentrates on lightweight and heavyweight behavior specification cases. JML distinguishes between

A lightweight specification case is similar to a behavior specification case, but with different defaults [Leavens-Baker-Ruby06]. It also is possible to desugar all such specification cases into behavior specification cases [Raghavan-Leavens05].


9.3 Access Control in Specification Cases

Heavyweight specification cases may be declared with an explicit access modifier, according to the following syntax.

 
privacy ::= public | protected | private

The access modifier of a heavyweight specification case cannot allow more access than the method being specified. So a public method may have a private behavior specification, but a private method may not have a public public specification. A heavyweight specification case without an explicit access modifier is considered to have default (package) access.

Lightweight specification cases have no way to explicitly specify an access modifier, so their access modifier is implicitly the same as the method being specified. For example, a lightweight specification of a public method has public access, implicitly, but a lightweight specification of a private method has private access, implicitly. Note that this is a different default than that for heavyweight specifications, where an omitted access modifier always means package access.

The access modifier of a specification case affects only which annotations are visible in the specification and does not affect the semantics of a specification case in any other way.

JML's usual visibility rules apply to specification cases. So, for example, a public specification case may only refer to public members, a protected specification case may refer to both public and protected members, as long as the protected members are otherwise accessible according to Java's rules, etc. See section 2.4 Privacy Modifiers and Visibility, for more details and examples.


9.4 Lightweight Specification Cases

Syntax

The following is the syntax of lightweight specification cases. These are the most concise specification cases.

 
lightweight-spec-case ::= generic-spec-case
generic-spec-case ::= [ spec-var-decls ]
                      spec-header
                      [ generic-spec-body ]
        | [ spec-var-decls ]
          generic-spec-body
generic-spec-body ::= simple-spec-body
        | {| generic-spec-case-seq |}
generic-spec-case-seq ::= generic-spec-case
                          [ also generic-spec-case ] ...
spec-header ::= requires-clause [ requires-clause ] ...
simple-spec-body ::= simple-spec-body-clause
                     [ simple-spec-body-clause ] ... 
simple-spec-body-clause ::= diverges-clause
        | assignable-clause | accessible-clause
        | captures-clause | callable-clause
        | when-clause | working-space-clause
        | duration-clause | ensures-clause
        | signals-only-clause | signals-clause
        | measured-clause 

As far as the syntax is concerned, the only difference between a lightweight specification case and a behavior-specification-case (see section 9.6 Behavior Specification Cases) is that the latter has the keyword behavior and possibly an access control modifier.

A lightweight specification case always has the same access modifier as the method being specified, see 9.3 Access Control in Specification Cases. To specify a different access control modifier, one must use a heavyweight specification.

Semantics

A lightweight specification case can be understood as syntactic sugar for a behavior specification case, except that the defaults for omitted specification clauses are different for lightweight specification cases than for behavior specification cases. So, for example, apart from the class names, method m in class Lightweight below
 
package org.jmlspecs.samples.jmlrefman;

public abstract class Lightweight {

    protected boolean P, Q, R;
    protected int X;

    /*@ requires P;
      @  assignable X;
      @  ensures Q;
      @  signals (Exception) R;
      @*/
    protected abstract int m() throws Exception;
}
has a specification that is equivalent to that of method m in class Heavyweight below.
 
package org.jmlspecs.samples.jmlrefman;

public abstract class Heavyweight {

    protected boolean P, Q, R;
    protected int X;

    /*@ protected behavior
      @   requires P;
      @   diverges false;
      @   assignable X;
      @   when \not_specified;
      @   working_space \not_specified;
      @   duration \not_specified;
      @   ensures Q;
      @   signals_only Exception;
      @   signals (Exception) R;
      @*/
    protected abstract int m() throws Exception;
}

As this example illustrates, the default for an omitted clause in a lightweight specification is \not_specified for all clauses, except diverges, which has a default of false, and signals [Leavens-Baker-Ruby06]. The default for an omitted signals clause is to only permit the exceptions declared in the method's header to be thrown. Thus, if the method declares that exceptions DE1 and DE2 may be thrown, then the default for an omitted signals clause is
 
  signals (Exception e) e instanceof DE1 || e instanceof DE2;
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 may decide to treat it as if it were false.

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.


9.5 Heavyweight Specification Cases

There are three kinds of heavyweight specification cases, called behavior, normal behavior, and exceptional behavior specification cases, beginning (after an optional privacy modifier) with the one of the keywords behavior, normal_behavior, or exceptional_behavior, respectively.

 
heavyweight-spec-case ::= behavior-spec-case
        | exceptional-behavior-spec-case
        | normal-behavior-spec-case

Like lightweight specification cases, normal behavior and exceptional behavior specification cases can be understood as syntactic sugar for special kinds of behavior specification cases [Raghavan-Leavens05].


9.6 Behavior Specification Cases

The behavior specification case is the most general form of specification case. All other forms of specification cases simply provide some syntactic sugar for special kinds of behavior specification cases.

Syntax

As far as the syntax is concerned, the only difference between a behavior specification case and a lightweight one is the optional access control modifier, privacy, and the keyword behavior (or the British variant, behaviour). One can use either the British or the American spelling of this keyword, although for historical reasons most examples will use the American spelling.

 
behavior-spec-case ::= [ privacy ] [ code ] behavior-keyword
                       generic-spec-case
behavior-keyword ::= behavior | behaviour

See section 16.2 Code Contracts, for details of the semantics of behavior-spec-cases that use the code keyword.

Semantics

To explain the semantics of a behavior specification case we make a distinction between flat and nested specification cases:

Invariants and constraints

The semantics of a behavior specification case for a method or constructor in a class depends on the invariants and constraints that have been specified. This is discussed in 8.2 Invariants and 8.3 Constraints. In a nutshell, methods must preserve invariants and respect constraints, and constructors must establish invariants.

9.6.1 Semantics of flat behavior specification cases  
9.6.2 Semantics of non-helper methods  
9.6.3 Semantics of non-helper constructors  
9.6.4 Semantics of helper methods and constructors  
9.6.5 Semantics of nested behavior specification cases  


9.6.1 Semantics of flat behavior specification cases

Below we explain the semantics of a simple behavior-spec-case case with precisely one requires clause, one diverges clause, one measured_by clause, one assignable clause, one accessible clause, one callable clause, one when clause, one ensures clause, one duration clause, one working_space clause, one signals_only clause, and one signals clause.

A behavior specification case can contain any number of these clauses, and there are defaults that allow any of them to be omitted. However, as explained in 9.9 Method Specification Clauses, any behavior specification case is equivalent with a behavior specification case of this form.


9.6.2 Semantics of non-helper methods

Consider a non-helper instance method m, and a specification case of the following form.
 
  behavior
    forall T1 x1; ... forall Tn xn;
    old U1 y1 = F1; ... old Uk yk = Fk;
    requires P;
    measured_by Mbe if Mbp;
    diverges D;
    when W;
    accessible R;
    assignable A;
    callable p1(...), ..., pl(...);
    captures Z;
    ensures Q;
    signals_only E1, ..., Eo;
    signals (E e) S;
    working_space Wse if Wsp;
    duration De if Dp;

The meaning of this specification case is as follows.

Consider a particular call of the method m.

The state of the program after passing parameters to m, but before running any of the code of m is called the pre-state of the method call.

Suppose all applicable invariants hold in the pre-state of this call.

For every possible value of the variables declared in the forall clauses, x1, ..., xn, the following must be true. (If there are no forall clauses, then the following just has to hold all by itself.)

Suppose that the variable y1 is bound to the pre-state value of F1 in the pre-state (i.e., the beginning of the method, after parameter passing), and in turn each of the old variable declarations are bound to the values of the corresponding expressions, also evaluated in the pre-state, and finally yk is bound to the value of Fk in the pre-state. These bindings can depend on previously defined old variable declarations in the specification case. (If there are no old clauses, then no such variables are bound.) We call the state with such bindings in place the augmented pre-state.

Suppose also that with these binding (i.e., in the augmented pre-state), that the precondition, P, from the requires clause, holds.

If the method has a measured_by clause, and if the predicate in the measured_by clause, Mbp, is true in the augmented pre-state, and if this call is in the control flow of another instance of this method, Caller, then the value of the expression Mbe in this call's augmented pre-state must be non-negative and strictly less than the value of Mbe in the pre-state of Caller. (If the measured_by clause is omitted, there is no such requirement.) For example, consider a method fib that calls itself directly and has an integer parameter n and for which the measured_by clause has n as its expression (Mbe), and the default predicate (Mbp) is true; then recursive calls of fib that appear in the body of fib must have actual argument exprssions whose value is (non-negative and) strictly less than n, such as n-1 and n-2.(8)

Then one of the following must also hold:

In all of these clauses, the value of a formal parameter is always considered to be the value they had in the pre-state. That is the actual post-state value they take in an execution is not considered, as explained in See section 9.9.6 Parameters in Postconditions.


9.6.3 Semantics of non-helper constructors

The semantics of a flat specification case for a (non-helper) constructor is the same as that for a (non-helper) method given above, except that:

These two differences are also discussed in 8.2 Invariants and 8.3 Constraints.


9.6.4 Semantics of helper methods and constructors

The semantics of a flat specification case for a helper method (or constructor) is the same as that for a non-helper method (or constructor) given above, except that:

These differences are also discussed in 8.2 Invariants and 8.3 Constraints.


9.6.5 Semantics of nested behavior specification cases

We now explain how all behavior specification cases can be desugared into a list of one or more flat specification cases joined by the also keyword [Raghavan-Leavens05]. The semantics of a behavior specification case is then simply the semantics of this desugared version.

The desugaring is as follows. Consider a specification of the form.

 
spec-var-decls
spec-header
{|
    GenSpecCase1 
  also 
    ... 
  also 
    GenSpecCasen 
|}

The above desugars to the following.

 
    spec-var-decls
    spec-header
    GenSpecCase1
  also 
    ... 
  also 
    spec-var-decls
    spec-header
    GenSpecCasen

In the above desugaring either the spec-var-decls or the spec-header (or both) may be omitted.

The meaning of the desugared list of specification cases is explained in 9.2 Organization of Method Specifications. The meaning of a single simple specification case is explained in 9.6.1 Semantics of flat behavior specification cases.


9.7 Normal Behavior Specification Cases

A normal_behavior specification case is just syntactic sugar for a behavior specification case with an implicit signals clause
 
    signals (java.lang.Exception) false;
ruling out abrupt termination, i.e., the throwing of any exception. Note that this includes unchecked exceptions, since in Java, RuntimeException is a subclass of Exception.

The following gives the syntax of the body of a normal behavior specification case.

 
normal-behavior-spec-case ::= [ privacy ] [ code ] normal-behavior-keyword
                              normal-spec-case
normal-behavior-keyword ::= normal_behavior | normal_behaviour
normal-spec-case ::= generic-spec-case

As far as syntax is concerned, the only difference between a normal-spec-case and a generic-spec-case is that normal behavior specification cases cannot include signals-clauses or signals-only-clauses.

The semantics of a normal behavior specification case is the same as the corresponding behavior specification case (see section 9.6 Behavior Specification Cases) with the addition of the following signals-clause

 
    signals (java.lang.Exception) false;

So a normal behavior specification case specifies a precondition which guarantees normal termination; i.e., it prohibits the method from throwing an exception.


9.8 Exceptional Behavior Specification Cases

The following gives the syntax of the body of an exceptional behavior specification case.

 
exceptional-behavior-spec-case ::= [ privacy ] [ code ] exceptional-behavior-keyword
                                   exceptional-spec-case
exceptional-behavior-keyword ::= exceptional_behavior | exceptional_behaviour
exceptional-spec-case ::= generic-spec-case

As far as syntax is concerned, the only difference between an exceptional-spec-case and a generic-spec-case is that exceptional behavior specification cases cannot include ensures-clauses.

The semantics of an exceptional behavior specification case is the same as the corresponding behavior specification case (see section 9.6 Behavior Specification Cases) with the addition of the following ensures clause.

 
    ensures false;

So an exceptional behavior specification case specifies a precondition which guarantees that the method throws an exception, if it terminates, i.e., a precondition which prohibits the method from terminating normally.

9.8.1 Pragmatics of Exceptional Behavior Specifications Cases  


9.8.1 Pragmatics of Exceptional Behavior Specifications Cases

Note that an exceptional behavior specification case says that some exception must be thrown if its precondition is met (assuming the diverges clause predicate is false, as is the default.) Beware of the difference between specifying that an exception must be thrown and specifying that an exception may be thrown. To specify that an exception may be thrown you should not use an exceptional behavior, but should instead use a behavior specification case [Leavens-Baker-Ruby06].

For example, the following method specification
 
package org.jmlspecs.samples.jmlrefman;

public abstract class InconsistentMethodSpec {

    /** A specification that can't be satisfied. */
    /*@  public normal_behavior
     @    requires z <= 99;
     @    assignable \nothing;
     @    ensures \result > z;
     @ also
     @  public exceptional_behavior
     @    requires z < 0;
     @    assignable \nothing;
     @    signals (IllegalArgumentException) true;
     @*/
    public abstract int cantBeSatisfied(int z)
        throws IllegalArgumentException;
}
is inconsistent because the preconditions z <= 99 and z < 0 overlap, for example when z is -1. When both preconditions hold then the exceptional behavior case specifies that an exception must be thrown and the normal behavior case specifies that an exception must not be thrown, but the implementation cannot both throw and not throw an exception.

Similarly, multiple exceptional specification cases with overlapping preconditions may give rise to an inconsistent specification. For example, the following method specification
 
package org.jmlspecs.samples.jmlrefman;

public abstract class InconsistentMethodSpec2 {

    /** A specification that can't be satisfied. */
    /*@  public exceptional_behavior
     @     requires z < 99;
     @     assignable \nothing;
     @     signals_only IllegalArgumentException;
     @ also
     @   public exceptional_behavior
     @     requires z > 0;
     @     assignable \nothing;
     @     signals_only NullPointerException;
     @*/
    public abstract int cantBeSatisfied(int z)
        throws IllegalArgumentException, NullPointerException;
}
is inconsistent because, again, the two preconditions overlap, and the signals_only clauses do not permit the same exception to be thrown in both cases.

There is an important distinction to be made between the signals and the signals_only clauses in JML. The signals_only clause says what exceptions may be thrown (when the specification case's precondition is met); this clause does not say anything about the state of the exception object or other locations in the system. On the other hand, the signals clause only describes what must be true of the system state when an exception is thrown, and does not say anything about what exceptions may be thrown. For example, consider the following specification.
 
package org.jmlspecs.samples.jmlrefman;

public abstract class SignalsClause {

    /*@ signals (IllegalArgumentException) x < 0;
      @ signals (NullPointerException) x < 0;
      @*/
    public abstract int notPrecise(int x) throws RuntimeException;
}
The above allows a method to throw either an IllegalArgumentException or a NullPointerException when x is less than 0, but in that condition the method might also throw a different exception altogether, as long as that exception was permitted by the method's declaration header. The only thing ruled out by this specification is throwing either a IllegalArgumentException or a NullPointerException when x is not less than 0. Thus from such a specification one may draw the conclusion that x < 0 only when one of these two exceptions is thrown.

Therefore, if one just wants to specify the exceptions that are permitted to be thrown in a specific situation, one should use the signals_only clause.


9.9 Method Specification Clauses

The different kinds of clauses that can be used in method specifications are discussed in this section. See section 9.4 Lightweight Specification Cases, for the overall syntax that ties these clauses together.

9.9.1 Specification Variable Declarations  
9.9.2 Requires Clauses  
9.9.3 Ensures Clauses  
9.9.4 Signals Clauses  
9.9.5 Signals-Only Clauses  
9.9.6 Parameters in Postconditions  
9.9.7 Diverges Clauses  
9.9.8 When Clauses  
9.9.9 Assignable Clauses  
9.9.10 Accessible Clauses  
9.9.11 Callable Clauses  
9.9.12 Measured By Clauses  
9.9.13 Captures Clauses  
9.9.14 Working Space Clauses  
9.9.15 Duration Clauses  


9.9.1 Specification Variable Declarations

The syntax of spec-var-decls is as follows.

 
spec-var-decls ::= forall-var-decls [ old-var-decls ]
        | old-var-decls
The scope of the variables declared in the spec-var-decls is the entire specification case in which they appear. The two types of such declarations are described below.

9.9.1.1 Forall Variable Declarations  
9.9.1.2 Old Variable Declarations  


9.9.1.1 Forall Variable Declarations

The syntax of the forall-var-decls is as follows.

 
forall-var-decls ::= forall-var-declarator [ forall-var-declarator ] ... 
forall-var-declarator ::= forall [ bound-var-modifiers ] type-spec quantified-var-declarator ;

When a forall-var-declarator is used, it specifies that the specification case that follows must hold for every possible value of the declared variables. In other words, it is a universal quantification over the specification case. See section 12.4.24 Quantified Expressions, for the syntax of quantified-var-declarator.

Note that if such variables are used in preconditions, then they can be thought to range over all values that satisfy the preconditions. The bound variable may not have the same name as earlier bound variables in the specification, nor may it shadow the formal parameters of the method declaration.


9.9.1.2 Old Variable Declarations

The syntax of the old-var-decls is as follows. See section 7.1.2.2 Type-Specs, for the syntax of type-spec. [[[Give cross ref for spec-variable-declarators when ready.]]]

 
old-var-decls ::= old-var-declarator [ old-var-declarator ] ...
old-var-declarator ::= old [ bound-var-modifiers ] type-spec spec-variable-declarators ;

An old-var-declarator allows abbreviation within a specification case. The names defined in the spec-variable-declarators can be used throughout the specification case for the values of their initializers. As the name suggests, the expressions are evaluated in the method's pre-state. The bound variable may not rename earlier bound variables in the specification, nor the formal parameters of the method declaration.

[[[Example]]]


9.9.2 Requires Clauses

A requires clause specifies a precondition of method or constructor. Its syntax is as follows.

 
requires-clause ::= requires-keyword pred-or-not ;
        | requires-keyword \same ;
requires-keyword ::= requires | pre 
        | requires_redundantly | pre_redundantly
pred-or-not ::= predicate | \not_specified

The predicate in a requires clause can refer to any visible fields and to the parameters of the method. See section 2.4 Privacy Modifiers and Visibility, for more details on visibility in JML.

Any number of requires clauses can be included a single specification case. Multiple requires clauses in a specification case mean the same as a single requires clause whose precondition predicate is the conjunction of these precondition predicates in the given requires clauses. For example,
 
  requires P;
  requires Q;
means the same thing as:
 
  requires P && Q;

When a requires clause is omitted in a specification case, a default requires clause is used. For a lightweight specification case, the default precondition is \not_specified. The default precondition for a heavyweight specification case is true.

At most one precondition in a specification case can use \same, and \same cannot be used in the only specification case for a method unless the method is an override (including overriding a specification from an interface). Similarly, \same cannot be used in the only specification case for a constructor or a static method. Another restriction is that \same cannot be used in a requires clause of a nested specification case (see section 9.6.5 Semantics of nested behavior specification cases).

When the precondition is \same in a specification case, it means that the specification case being written has, effectively, the same precondition as that specified in the other (non-\same) specification cases. That is, \same stands for the disjunction (with ||) of the preconditions in all non-\same specification cases of the method's specification from the current class together with the inherited specification cases defined in its supertypes (i.e., in its superclasses and implemented interfaces). The order of this disjunction has, from left to right, inherited preconditions before each of the preconditions from the specification of any method that overrides it.


9.9.3 Ensures Clauses

An ensures clause specifies a normal postcondition, i.e., a property that is guaranteed to hold at the end of the method (or constructor) invocation in the case that this method (or constructor) invocation returns without throwing an exception. The syntax is as follows See section 9.9.2 Requires Clauses, for the syntax of pred-or-not.

 
ensures-clause ::= ensures-keyword pred-or-not ;
ensures-keyword ::= ensures | post
        | ensures_redundantly | post_redundantly

A predicate in an ensures clause can refer to any visible fields, the parameters of the method, \result if the method is non-void, and may contain expressions of the form \old(E). See section 2.4 Privacy Modifiers and Visibility, for more details on visibility in JML.

Informally,
 
  ensures Q;
means

if the method invocation terminates normally (ie. without throwing an exception), then predicate Q holds in the post-state.

In an ensures clause, \result stands for the result that is returned by the method. The postcondition Q may contain expressions of the form \old(e). Such expressions are evaluated in the pre-state, and not in the post-state, and allow Q to express a relation between the pre- and the post-state. If parameters of the method occur in the postcondition Q, these are always evaluated in the pre-state, not the post-state. In other words, if a method parameter x occurs in Q, it is treated as \old(x). For a detailed explanation of this see 9.9.6 Parameters in Postconditions.

Any number of ensures clauses can be given in a single specification case. Multiple ensures clauses in a specification case mean the same as a single ensures clause whose postcondition predicate is the conjunction of the postcondition predicates in the given ensures clauses. So
 
  ensures P;
  ensures Q;
means the same as
 
  ensures P && Q;
Note that, in JML's semantics for expressions within assertions, the order of evaluation of P and Q does not matter. See section 2.7 Expression Evaluation and Undefinedness, for more details on this topic.

When an ensures clause is omitted in a specification case, a default ensures clause is used. For a lightweight specification case, the default precondition is \not_specified. The default precondition for a heavyweight specification case is true.


9.9.4 Signals Clauses

In a specification case a signals clause specifies the exceptional or abnormal postcondition, i.e., the property that is guaranteed to hold at the end of a method (or constructor) invocation when this method (or constructor) invocation terminates abruptly by throwing a given exception.

The syntax is as follows. See section 9.9.2 Requires Clauses, for the syntax of pred-or-not.

 
signals-clause ::= signals-keyword ( reference-type [ ident ] )
                   [ pred-or-not ] ;
signals-keyword ::= signals | signals_redundantly
        | exsures | exsures_redundantly

In a signals-clause of the form
 
  signals (E e) P;
E has to be a subclass of java.lang.Exception, and the variable e is bound in P. If E is a checked exception (i.e., if it does not inherit from java.lang.RuntimeException [Arnold-Gosling-Holmes00] [Gosling-etal00]), it must either be one of the exceptions listed in the method or constructor's throws clause, or a subclass or a superclass of such a declared exception.

Informally,
 
  signals (E e) P;
means

If the method (or constructor) invocation terminates abruptly by throwing an exception of type E, then predicate P holds in the final state for this exception object E.

A signals clause of the form
 
  signals (E e) R;
is equivalent to the signals clause
 
  signals (java.lang.Exception e) (e instanceof E) ==> R;

Several signals clauses can be given in a single lightweight, behavior or exceptional behavior specification case. Multiple signals clauses in a specification case mean the same as a single signals clause whose exceptional postcondition predicate is the conjunction of the exceptional postcondition predicates in the given signals clauses. This should be understood to take place after the desugaring given above, which makes all the signals clauses refer to exceptions of type java.lang.Exception. Also, the names in the given signals clauses have to be standardized [Raghavan-Leavens05]. So for example,
 
  signals (E1 e) R1;
  signals (E2 e) R2;
means the same as
 
  signals (Exception e)   ((e instanceof E1) ==> R1)
                       && ((e instanceof E2) ==> R2);
Note that this means that if an exception is thrown that is both of type E1 and of type E2, then both R1 and R2 must hold.

[[[EXAMPLE]]]

Beware that a signals clause specifies when a certain exception may be thrown, not when a certain exception must be thrown. To say that an exception must be thrown in some situation, one has to exclude that situation from other signals clauses and from ensures clause (and any diverges clauses). It may also be useful to use the signals_only clause in such specifications (see section 9.9.5 Signals-Only Clauses).

[[[EXAMPLE?]]]

When a behavior or exceptional specification case has no signals-clause, a default signals clause is used. For a heavyweight specification case, the default signals clause is signals (Exception) true;. Since normal behavior specification cases do not have signals clauses, no default applies for such specification cases. For a lightweight specification case, the default is signals \not_specified;.


9.9.5 Signals-Only Clauses

A signals_only clause is an abbreviation for a signals-clause (see section 9.9.4 Signals Clauses) that specifies what exceptions may be thrown by a method, and thus, implicitly, what exceptions may not be thrown.

The syntax is as follows.

 
signals-only-clause ::= signals-only-keyword reference-type [ , reference-type ] ... ;
        | signals-only-keyword \nothing ;
signals-only-keyword ::= signals_only | signals_only_redundantly

All of the reference-types named in a signals-only-clause must be subtypes of java.lang.Exception. Each reference-type that is a checked exception type (i.e., that does not inherit from java.lang.RuntimeException [Arnold-Gosling-Holmes00] [Gosling-etal00]), must either be one of the exceptions listed in the method or constructor's throws clause, or a subclass or a superclass of such a declared exception.

A signals-only-clause of the form
 
  signals_only E1, E2, ..., En;
is considered to be an abbreviation (syntactic sugar) for the following signals clause (see section 9.9.4 Signals Clauses).
 
  signals (java.lang.Exception e)
           e instanceof E1
        || e instanceof E2
        || ...
        || e instanceof En;
That is, such a clause specifies that if the method or constructor throws an exception, it must be an instance of one of the types named.

Several signals-only-clauses can be given in a single lightweight, behavior or exceptional behavior specification case. Multiple such clauses in a specification case mean the same as a single clause whose list contains only the names Ej that are subtypes of some type named in all of the given signals-only-clauses. Thus, the meaning is a kind of intersection of the signals_only clauses. Since this may be confusing, only one signals_only clause should ever be used in a given specification case.

The signals_only clause is useful for specifying when a certain exception, or one of a small set of exceptions, must be thrown. To say that an exception must be thrown in some situation, one has to exclude the method from returning normally in that situation (using an ensures clause or the precondition of some other specification case) and from not terminating (by using the diverges clause).

[[[Example]]]

If the signals_only is omitted from a specification case, a default signals_only clause is provided. The same default is used for both lightweight and heavyweight behavior and exceptional behavior specification cases. (Since normal behavior specification cases cannot throw exceptions at all, there is no default signals_only clause for such specification cases.) This default prohibits any exception not declared by the method in the method's header from being thrown. Thus the exact default depends on the method header. If the method header does not list any exceptions that can be thrown, then the default 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 DE_1, ..., DE_n, Err_1, ..., Err_m, where each DE_i is a subtype of java.lang.Exception, and each Err_j is not a subtype of java.lang.Exception, then the default signals_only clause is as follows.
 
   signals_only DE_1, ..., DE_n
For example, if the method has the header
 
   public void foo() throws E1, E2
then the default signals_only clause would be
 
   signals_only E1, E2;

It is important to note that the set of exceptions included in the default signals clause described above never includes java.lang.Throwable, and does not include java.lang.Error or any of its subtypes. Furthermore, this default would not normally include java.lang.RuntimeException or any of its subtypes, because Java explicitly allows RuntimeExceptions to be thrown even if they are not declared in the method header's throws clause. Since such unchecked, runtime exceptions are not usually listed in the method header, they would not find their way into the default signals_only clause. In JML, however, if you wish to allow such runtime exceptions, you can either explicitly list them in the method header or, more usually, you would list them in an explicit signals_only clause.


9.9.6 Parameters in Postconditions

Parameters of methods are passed by value in Java, meaning that parameters are local variables in a method body, which are initialized when the method is called with the values of the parameters for the invocation.

This leads us to the following two rules:

The justification for the first convention is that clients cannot observe assignments to the parameters anyway, as these are local variables that can only be used by the implementation of the method. Given that clients can never observe these assignments, there is no point in making them part of the contract between a class and its clients.

The justification for the second convention is that clients only know the initial values of the parameter that they supply, and do not have any knowledge of the final values that these variables may have in the post-state.

The reason for this is best illustrated by an example. Consider the following class and its method specifications. Without the convention described above the implementations given for methods notCorrect1 and notCorrect2 would satisfy their specifications. However, clearly neither of these satisfies the specification when read from the caller's point of view.

 
package org.jmlspecs.samples.jmlrefman;

public abstract class ImplicitOld {

    /*@ ensures 0 <= \result && \result <= x;
      @ signals (Exception) x < 0;
      @*/
    public static int notCorrect1(int x) throws Exception {
        x = 5;
        return 4;
    }

    /*@ ensures 0 <= \result && \result <= x;
      @ signals (Exception) x < 0;
      @*/
    public static int notCorrect2(int x) throws Exception {
        x = -1;
        throw new Exception();
    }

    /*@ ensures 0 <= \result && \result <= x;
      @ signals (Exception) x < 0;
      @*/
    public static int correct(int x) throws Exception {
        if (x < 0) {
            throw new Exception();
        } else {
            return 0;
        }
    }
}

The convention above rules out such pathological implementations as notCorrect1 above; because mention of a formal parameter name, such as x above, in postconditions always means the pre-state value of that name, e.g., \old(x) in the example above.


9.9.7 Diverges Clauses

The diverges clause is a seldom-used feature of JML. It can be used to specify when a method may either loop forever or not return normally to its caller. The syntax is as follows See section 9.9.2 Requires Clauses, for the syntax of pred-or-not.

 
diverges-clause ::= diverges-keyword pred-or-not ;
diverges-keyword ::= diverges | diverges_redundantly

When a diverges clause is omitted in a specification case, a default diverges clause is used. For both lightweight and heavyweight specification cases, the default diverges condition is false. Thus by default, specification cases give total correctness specifications [Dijkstra76]. Explicitly writing a diverges clause allows one to obtain a partial correctness specification [Hoare69]. Being able to specify both total and partial correctness specification cases for a method leads to additional power [Hesselink92] [Nelson89].

As an example of the use of diverges, consider the abort method in the following class. (This example is simplified from the specification of Java's System.exit method. This specification says that the method can always be called (the implicit precondition is true), may always not return to the caller (i.e., diverge), and may never return normally, and may never throw an exception. Thus the only thing the method can legally do, aside from causing a JVM error, is to not return to its caller.

 
package org.jmlspecs.samples.jmlrefman;
 
public abstract class Diverges {

    /*@ public behavior
      @    diverges true;
      @    assignable \nothing;
      @    ensures false;
      @    signals (Exception) false;
      @*/
    public static void abort();

}

The diverges clause is also useful to specify things like methods that are supposed to abort the program when certain conditions occur, although that isn't really good practice in Java. In general, it is most useful for examples like the one given above, when you want to say when a method cannot return to its caller.


9.9.8 When Clauses

The when clause allows concurrency aspects of a method or constructor to be specified [Lerner91] [Rodriguez-etal05]. A caller of a method will be delayed until the condition given in the when clause holds. What is checked is that the method does not proceed to its commit point, which is the start of execution of statement with the label commit, until the given predicate is true.

The syntax is as follows. See section 9.9.2 Requires Clauses, for the syntax of pred-or-not.

 
when-clause ::= when-keyword pred-or-not ;
when-keyword ::= when | when_redundantly

When a when clause is omitted in a specification case, a default when clause is used. For a lightweight specification case, the default when condition is \not_specified. The default when condition for a heavyweight specification case is true.

See [Rodriguez-etal05] for more about the when clause and JML's plans for support of multithreading.


9.9.9 Assignable Clauses

An assignable clause gives a frame axiom for a specification. It says that, from the client's point of view, only the locations named, and locations in the data groups associated with these locations, can be assigned to during the execution of the method. The values of all subexpressions used in assignable clauses, such as i-1 in a[i-1], are computed in the pre-state of the method, because the assignable clause only talks about locations that exist in the pre-state.

See section 10. Data Groups, for more about specification of data groups. However, locations that are local to the method (or methods it calls) and locations that are created during the method's execution are not subject to this restriction.

The syntax is as follows. See section 12.7 Store Refs, for the syntax of store-ref-list.

 
assignable-clause ::= assignable-keyword store-ref-list ;
assignable-keyword ::= assignable | assignable_redundantly
        | modifiable | modifiable_redundantly
        | modifies | modifies_redundantly

When an assignable clause is omitted in a specification case, a default assignable clause is used. This default has a default store-ref-list. For a lightweight specification case, the default store-ref-list is \not_specified. The default store-ref-list for a heavyweight specification case is \everything.

If one wants the opposite of the default (for a heavyweight specification case), then one can specify that a method cannot assign to any locations by writing:
 
  assignable \nothing;
Using the modifier pure on a method achieves the same effect as specifying assignable \nothing, but does so for the method's entire specification as opposed to a single specification-case.

Assignable clauses are subject to several restrictive rules in JML. The first rule has to do with fields of model objects. Because model objects are abstract and do not have a concrete state or concrete fields, the JML typechecker does not allow fields of model objects to be listed in the assignable clause; that is, such expressions do not specify a set of locations (concrete fields) that can be assigned to. Thus expressions like f.x are not allowed in the assignable clause when f is a model field.

[[[Flesh out other restrictions. Refer to [Mueller-Poetzsch-Heffter-Leavens03] for details.]]]


9.9.10 Accessible Clauses

The accessible clause is a seldom-used feature of JML. Together with the assignable clause (see section 9.9.9 Assignable Clauses), it says what (pre-existing) locations a method may read during its execution. It has the following syntax.

 
accessible-clause ::= accessible-keyword store-ref-list ;
accessible-keyword ::= accessible | accessible_redundantly

During execution of the method (which includes all directly and indirectly called methods and constructors), only locations that either did not exist in the pre-state, that are local to the method (including the method's formal parameters), or that are either named in the lists found in the accessible and assignable clauses or that are dependees (see section 10. Data Groups) of such locations, are read from. Note that locations that are local to the method (or methods it calls) and locations that are created during the method's execution are not subject to this restriction and may be read from freely.

When an accessible clause is omitted in a code contract specification case, a default accessible clause is used. This default has a default store-ref-list which is \everything.

See section 16. Specification for Subtypes, for more discussion and examples.


9.9.11 Callable Clauses

The callable clause says what methods may be called, either directly or indirectly, by the method being specified. It has the following syntax.

 
callable-clause ::= callable-keyword callable-methods-list ;
callable-keyword ::= callable | callable_redundantly
callable-methods-list ::= method-name-list | store-ref-keyword

During execution of a method, the only methods and constructors that may be called are those listed in the callable clause's list.

When a callable clause is omitted in a code contract specification case, a default callable clause is used. This default has a default callable-methods-list which is \everything.

See section 16. Specification for Subtypes, for more discussion and examples.


9.9.12 Measured By Clauses

A measured by clause can be used in a termination argument for a recursive specification. It has the following syntax.

 
measured-clause ::= measured-by-keyword \not_specified ;
        | measured-by-keyword spec-expression [ if predicate ] ;
measured-by-keyword ::= measured_by | measured_by_redundantly

The spec-expression in a measured by clause must have type int.

In both lightweight and heavyweight specification cases, an omitted measured by clause means the same as a measured by clause of the following form.
 
    measured_by \not_specified;


9.9.13 Captures Clauses

The captures clause has the following syntax.

 
captures-clause ::= captures-keyword store-ref-list ;
captures-keyword ::= captures | captures_redundantly

The captures clause says that references to the store-refs listed can be retained after the method returns, for example in a field of the receiver object or in a static field. Therefore, the captures clause specifies when an object, passed as an actual parameter in a method call, may be captured during the call.

An actual parameter object (including the receiver this) is captured if it appears on the right-hand side of an assignment statement during the call. This can also happen indirectly through another method or constructor call or by returning the parameter object as the method result (we assume the result will be assigned to a field or local variable after the call).

The captures clause is used to prevent certain kinds of representation exposure as part of an alias control technique. For example, if an object should not be aliased, then that object must not be passed to a method that may capture it, i.e., may create an alias to it (this includes the receiver). Furthermore, objects used as part of the abstract representation of a type should not be aliased, and thus should not be passed to methods that capture it. JML tools will eventually prevent such aliasing.

When a captures clause is omitted in a method specification case, then a default captures clause is used. This default has a default store-ref-list which is \everything. Thus when omitted, a method is allowed to capture any of the actual parameter objects or the receiver.


9.9.14 Working Space Clauses

A working-space-clause can be used to specify the maximum amount of heap space used by a method, over and above that used by its callers. The clause applies only to the particular specification case it is in, of course This is adapted from the work of Krone, Ogden, and Sitaraman on RESOLVE [Krone-Ogden-Sitaraman03].

 
working-space-clause ::= working-space-keyword \not_specified ;
        | working-space-keyword spec-expression [ if predicate ] ;
working-space-keyword ::= working_space | working_space_redundantly

The spec-expression in a working space clause must have type long. It is to be understood in units of bytes.

The spec-expression in a working space clause may use \old and other JML operators appropriate for postconditions. This is because it is considered to be evaluated in the post-state, and provides a guarantee of the maximum amount of additional space used by the call. In some cases this space may depend on the \result, exceptions thrown, or other post-state values. [[[ There is however no way to identify the exception thrown - DRCok]]]

In both lightweight and heavyweight specification cases, an omitted working space clause means the same as a working space clause of the following form.
 
    working_space \not_specified;

See section 12.4.13 \working_space, for information about the \working_space expression that can be used to describe the working space needed by a method call. See section 12.4.12 \space, for information about the \space expression that can be used to describe the heap space occupied by an object.


9.9.15 Duration Clauses

A duration clause can be used to specify the maximum (i.e., worst case) time needed to process a method call in a particular specification case. [[[ Tools are simpler if the argument can simply be an arbitrary expression rather than a method call. -- DRCok ]]] This is adapted from the work of Krone, Ogden, and Sitaraman on RESOLVE [Krone-Ogden-Sitaraman03].

 
duration-clause ::= duration-keyword \not_specified ;
        | duration-keyword spec-expression [ if predicate ] ;
duration-keyword ::= duration | duration_redundantly

The spec-expression in a duration clause must have type long. It is to be understood in units of [[[the JVM instruction that takes the least time to execute, which may be thought of as the JVM's cycle time.]]] The time it takes the JVM to execute such an instruction can be multiplied by the number of such cycles to arrive at the clock time needed to execute the method in the given specification case. [[[This time should also be understood as not counting garbage collection time.]]]

The spec-expression in a duration clause may use \old and other JML operators appropriate for postconditions. This is because it is considered to be evaluated in the post-state, and provides a guarantee of the maximum amount of additional space used by the call. In some cases this space may depend on the \result, exceptions thrown, or other post-state values. [[[ There is no way to identify the exception thrown - DRCok]]]

In both lightweight and heavyweight specification cases, an omitted duration clause means the same as a duration clause of the following form.
 
    duration \not_specified;

See section 12.4.11 \duration, for information about the \duration expression that can be used in the duration clause to specify the duration of other methods.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html