Contracts are used to specify the client-visible behavior of an object without saying anything about how this behavior is implemented. For JContractS contracts are specified as assertions attached to Javadoc tags in Javadoc comments. There are three types of contracts: preconditions, postconditions and invariants. The purpose of each type is explained below.
Multiple Javadoc tags of the same type are allowed. If you specify multiple tags, the tags of the same type will be evaluated in the order specified. If an assertion fails the following assertions will not be evaluated. This way assertions can be used that assume the conditions of preceding assertions hold. It works the same as conditional logical operator where following terms can assume the preceding terms held.
The assertions are written using standard Java expression with some extensions. The extensions are explained in following sections.
An invariant describes what assertions must hold during the lifetime of an object. It describes the valid state of an object. The assertions do not have to hold all the time, it is allowed for a method to temporarily change the object to an invalid state. But after the method has finished, the object must have a state that is valid according to the assertions of the invariant. More specifically, the invariant is checked after creation and after invocation of a public method. This allows protected, package-visible and private methods to change the object as they see fit.
The invariant is added to the Javadoc comment of the type. The assertions of an invariant are preceded by the
Javadoc tag @inv. Here is the invariant for a (simple) stack:
/**
* @inv getSize() >= 0
*/
public interface Stack
{
...
}
This invariant states that the size will always be a non-negative integer.
A precondition is used to state when it is valid to invoke a method. It is used in addition to the invariant which must hold for all methods. The precondition usually ensures that a method is only invoked when the object is in the correct state for that method, and that the parameters passed are valid. A method only has to work correctly when its precondition holds. If the precondition does not hold then the result of the method is unpredictable.
Preconditions are added to the Javadoc comment of methods. They are preceded by the Javadoc tag
@pre. Here is the precondition for method pop() of a stack:
/** * @pre getSize() > 0 */ Object pop();
This preconditions states that it is only valid to invoke pop() when getSize()
returns a value greater than zero.
A postcondition states what the correct behavior of a method is. It is used in addition to the invariant which must hold for all methods. The postcondition usually ensures that a method changes the state of an object correctly, and that the return value is valid. If the method was called when the precondition held, the method is required to ensure that its postcondition (and the invariant) will hold.
Just like preconditions, postconditions are added to the Javadoc comment of methods. Postconditions are
preceded by the Javadoc tag @post. Here is the postcondition of pop():
/** * @post return != null */ Object pop();
The postcondition states that pop() will never return a value that is null.
Here is the full source code for a simple stack interface:
/**
* @inv getSize() >= 0
*/
public interface Stack
{
/**
* @post return >= 0
*/
int getSize();
/**
* @pre element != null
*/
void push(Object element);
/**
* @pre getSize() > 0
* @post return != null
*/
Object pop();
}
It is often very useful to describe the new state of an object in postconditions in terms of its previous
state. Take the postcondition of push(Object) and pop() for example, in addition to the
postconditions that were specified above it is useful to add postconditions that state that the size of the stack
has increased and decreased respectively.
For this purpose a special expression is present that allows capturing the value of an expression from before
the method invocation. To capture the value of an expression, append @pre to it. Here is the new
postcondition of push(Object):
/** * @post getSize() == getSize()@pre + 1 */ void push(Object element)
And here is the extended postcondition of pop():
/** * @post return != null * @post getSize() == getSize()@pre - 1 */ Object pop()
An operator that is very useful in assertions but is missing from Java is the implies operator. This operator can be used to state that an expression q, must hold if expression p holds. But if p does not hold, q is allowed to either hold or not.
Suppose you have an object that can either be enabled or disabled. When the object is disabled it must have a reason why it was disabled. Using implies it is easy and intuitive to specify this in the precondition of the method that changes the state.
/** * @pre !enable implies reason != null */ void setState(boolean enable, String reason);
Although this operator can also be written as !p || q, it is very useful to have a separate
operator for it because it reveals the intention better. Compare the precondition above with its rewritten
version:
/** * @pre enable || reason != null */ void setState(boolean enable, String reason);
Besides single-value fields/parameters collections of values are also used. It must be possible to state something about the values in these collections too. This requires iterating over a collection in an assertion. As this is very cumbersome and verbose, additional operators have been added to JContractS to make this easier.
These operators are called quantifiers and there are two variants: forall and
exists.
A forall expression holds if an assertion holds for each and every element in the collection.
Suppose you have a method that only works on collections of non-negative integers. You can add an assertion to the precondition that will verify that clients do not pass collections with negative integers:
/** * @pre forall Integer i in values | i.intValue() >= 0 */ List squareRoots(List values);
An exists expression holds if an assertion holds for at least one element in the collection.
Suppose you book groups of people into a hotel, but a group is only allowed to make a reservation if at least one of them is an adult.
/** * @pre exists Person p in people | p.getAge() >= 18 */ void book(Set people);