Class and Method Specifications



This handout describes how to document the specifications of classes and methods, focusing on practical issues.

This document uses a Line class as an example. We do not provide fields or method bodies in our example. This document covers specifying the behavior of classes and methods (what they should do), not their implementation (what they actually do and how they do it). Abstraction Functions and Representation Invariants covers how to document a class's implementation

 * This class represents the mathematical concept of a line segment. Think of
 * this as a pair (start-point, end-point), containing the starting and ending
 * points of the line.
 * Abstract Invariant:
 *  A line's start-point must be different from its end-point.
public class Line {

  ... // Fields not shown.

  * @spec.requires p != null && ! p.equals(start-point)
  * @spec.modifies this
  * @spec.effects Sets end-point to p
  public void setEndPoint(Point p) {



Because the concepts discussed here are interrelated, this document starts with a short list of definitions before diving into the details.

The above concepts are included in a class's external specification (in Javadoc comments). They help document for clients how to use the class.

The rest of this document is organized as follows. First, it explains how to document what a class abstractly represents using abstract state. Then, it explains how to specify method behavior, in terms of abstract state.

Abstract Values and Abstract State

The abstract value of an object is the mathematical concept that clients use to understand and reason about the object. For example, a line segment represents the set of points in the plane that lie on a particular line and in between two particular end points. In the computer, every object is a series of zeros and ones, but these represent higher-level ideas, their abstract values.

The abstract state of an object is the specific mathematical shape we use to define the abstract value for the client. In the example above, we defined the abstract state as a pair of points (start-point, end-point). This is just four numbers; however, the "meaning" of that pair (the abstract value) is really all the points in the plane that lie in between those two points, not just the two end points.

This abstract state does not necessarily imply that the concrete representation of the object is a pair of points. That is one concrete representation, but there are others, such as a start point, an angle, and a length. Abstract states typically describe the object at a less detailed level than the implementation so that clients can reason about only the concepts that are necessary to check that their own code is correct.

As another example, clients of String may only need to know that a string is a sequence of characters, not whether that sequence is implemented with an array, a linked list, a combination of the two, or some completely different way. The notion of sequence is more abstract than particular ways to represent sequences. How the String "cat" is represented concretely (within the Java code) does not affect its abstract state. Whether String internally uses an array, a List, or some clever compressed numerical encoding for the the characters 'c', 'a', and 't', the abstract state of "cat" is still a just a sequence of those letters.

Mathematical Notation

For some ADTs, the abstract values are well-described by concepts and notation that are common in mathematics and well-understood by software developers. Examples include:

If you are specifying such a class, then you're in luck. You can use conventional notation for specifying the class's abstract values and methods. Such notation includes:

You aren't obliged to use this syntax. Some of it is more standard than the rest: set-comprehension syntax is standard in just about all of mathematics, but sequence concatenation isn't particularly standardized. You may find it clearer to write sequence concatenation as a function like concat(x, y). What really matters is clarity and lack of ambiguity, so if you have any doubt whether your reader will understand you, just define it: “...where concat(x,y) is the concatenation of two sequences x and y.”


In the example above, we also implicitly defined names for the two endpoints: by defining the abstract state as (start-point, end-point), we were saying that we would refer to the first point in the pair as "start-point" and the second point in the pair as "end-point".

You can define names implicitly like this if you want, or you can write out more explicit definitions of the terminology that you will use to talk about the abstract states of your objects. The only strict requirement is to make sure that you are communicating clearly to the client. Misunderstandings between yourself and the client can easily lead to bugs.

Method Specifications

Method specifications describe the behavior of a method in terms of its preconditions and postconditions. Note that method specifications may refer to abstract states, method arguments, and global variables (also known as public static fields), but never to the concrete fields of the implementation - the client should not need knowledge of these concrete fields.


Preconditions are properties that must be true when the method is called. It is the responsibility of the caller to guarantee that these properties hold. If the preconditions do not hold, the method is allowed to behave in absolutely any fashion, including crashing the program, continuing with incorrect results, informing the user of the problem, or gracefully recovering from the problem. Callers should always assume that preconditions are not checked by a method. However, it is good practice — though not required — for an implementation to check its preconditions (if the check can be performed efficiently) and throw an exception if they are not satisfied.

Preconditions are indicated by the "requires" clause in a method specification. If a "requires" clause is omitted from the method specification, it is assumed that the method does not have any preconditions.

@spec.requires (default: no constraints)
The preconditions that must be met by the method's caller.

The CSE 331 specification style doesn't include @param, but it's good to write it in Javadoc anyway, because that is good Java style. Javadoc's @param cannot express preconditions about global state and is sometimes inconvenient for preconditions that relate multiple formal parameters, such as "elt is a member of list". Because @spec.requires is needed whether or not @param exists, the CSE 331 specification style puts all the preconditions into @spec.requires, to simplify explanations and so there is only one place to look for preconditions.


Postconditions are properties that a method guarantees will hold when the method exits. However, if the precondition did not hold when the method was called, then nothing else is relevant, and the method may behave in any fashion whatsoever. In particular, if the precondition does not hold upon method entry, then the postcondition need not hold on method exit.

A postcondition can be written as a single complex logical formula, but it is convenient to separate it into logically distinct parts. CSE 331 uses "return", "effects", "throws", and "modifies". (In the descriptions below, "default" indicates what is assumed if that clause is omitted from the method specification.)

@returns (default: no constraint on what is returned)
The value returned by the method, if any.
@throws (default: none, which means that no exceptions are ever thrown)
The exceptions that may be raised, and under which conditions. The specification should not make guarantees about the behavior when the preconditions are not satisfied.
@spec.modifies (default: nothing, which means that there are no side effects)
Objects whose abstract value may be modified by the procedure. They are not guaranteed to be modified, unless otherwise indicated by the effects clause. Usually, programmers are more interested in objects that are not listed in the modifies clause, since those are guaranteed not to be changed by the method.
@spec.effects (default: true, which means "can have any effect" on the references listed under modifies)
The side effects of the method, such as changes to the state of the current object, to parameters, or to objects held in global variables. If an object is listed in the modifies clause but not in the effects clause, then it may take on any value allowed by the abstract invariants of this class of objects. The difference between the modifies and effects causes is that modifies lists everything that may change and effects indicates what changes occur.

Subclasses and overridden methods

A subclass often has a different (stronger) specification than its superclass, and often has a larger abstract state than its superclass. When the specification and abstract state are identical to those of the parent (for instance, an implementation of an abstract class), then there is no need to repeat them in the subclass. However, it is helpful to include a brief note indicating that the superclass documentation should be used instead. That note helps readers to distinguish whether the specification is the same, or the author simply didn't document the class.

When the specifications differ, then you have two options. The first option is to repeat, in the subclass, the full superclass documentation. The advantage is that everything is in one place, which may improve understanding. The second option is to augment the existing specification — for example, to add new abstract invariants. Whichever you do, make sure that you clearly indicate your approach, and that you are consistent throughout the codebase.

Similar rules hold for a method that overrides another method. It is acceptable to omit the Javadoc comment if the specification is identical. (The generated HTML will use the overridden method's Javadoc documentation, but a normal Java comment is a good hint to someone who is reading the source code.) Otherwise, it is usually better to give the complete specification. If you merely augment the overridden method's specification, be sure to refer to it in the documentation.