In our previous post, we explained how important it is to write good documentation for your code. We also highlighted that documentation is often written in a way that makes it useless.

Here we take a look at how writing effective documentation for methods, i.e. its specification.

Method specification

The specification of a method describes its behavior in terms of preconditions and postconditions.

Preconditions (or pre) are the assumptions that the method makes on the input values and the current instance (this). They are thus properties that any caller of the method must guarantee to be true when she calls the method.

Postconditions (or post) are all the effects, return values and thrown exceptions that the method guarantees when it terminates, provided that the preconditions are satisfied. If that is not the case, the behavior of the method is undefined.

Pre and post constitute a contract between the caller and the method, according which the satisfaction of pre by the caller implies the satisfaction of post by the method.

The caller should never assume that the method checks that preconditions hold, although according to good practices the method should do so (more on defensive programming in a future post).

Writing preconditions

To distinguish pre within the documentation of a given method, we place the tag @requires before the actual preconditions. For instance, the following sample specifies that the method squareRoot does not accept a negative input value:

 * @requires x > 0
 * @return y +- 0.0001 such that x = y * y
double squareRoot(double x)

If the precondition is not met, there is no guarantee on the behavior of the method. Indeed, the square root of a negative real number is not a real number.

When there is no precondition documented, it means that the method can be called in any situation and with any input values.

Writing postconditions

Postconditions are often longer to write than pre. It is therefore helpful to write them in a more structured way. We propose to separate them in four blocks (also named clauses) tagged as follows: @modifies, @effects, @return and @throws.

@modifies specifies which variables are modified by the method, typically “this” or an input parameter. It allows one to see these variables at a glance rather than by reading long sentences.

@effects describes how each variable listed in the modifies clause is modified by the method, that is, the method side effects. If the clauses @modifies and @effects are not written, it means that the method has no side effects.

@return specifies what value is returned by the method w.r.t. the parameter values and the current instance. Not writing this clause means that the method returns nothing.

@throws indicates the exceptions that are thrown by the method and under which conditions they are thrown. If this clause is not written, it means that the method throws no exception.

For example, consider the following specification:

 * @modifies elts
 * @effects Sorts the elements of elts in ascending order, e.g.,
 *          if elts = [4,2,5,2] before the call, on return elts = [2,2,4,5]
 * @throws NullPointerException if elts is null
void sort(int[] elts)

In the sort method above, the @requires clause is missing, meaning that there is no precondition.

The @modifies clause states that the array elts may be modified by the method, while the @effects clause describes how the elements are sorted.

Finally the @throws clause handles the case where elts is a null reference, and throws an appropriate exception. The caller can thus pass a null object without violating any precondition, given that the method takes responsibility for handling null values.


How would you document your methods? What’s your opinion about this way of documenting?