Contents:
This article describes how to document the specifications of methods using javadoc. The specification documents the intended behavior of methods — i.e., what they should do — rather than their implementation — i.e., what they actually do (and how they do it).
As we saw in class, method specifications describe the behavior of a method in terms of its preconditions and postconditions.
Preconditions are assertions that must hold when the method is called. It is the responsibility of the caller to guarantee that they do. If the preconditions do not hold, then the method is allowed to behave in absolutely any fashion, including crashing the program.
Callers should always assume that preconditions are not checked by the method, as it is the caller's responsibility to ensure that the preconditions are always satisfied. However, it is often a good idea 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.
(In the descriptions above and below, "default" indicates what is assumed if that clause is omitted from the method specification.)
Postconditions are assertions that the method guarantees will hold when the method exits, assuming that the preconditions held initially. If the precondition did not hold when the method was called, then nothing is promised. In other words, 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".
See the document on class specifications to learn how to talk about the states of objects in these clauses.
The assertions that appear in "effects" constrain the changes that are allowed to be made by the method. In general, more assertions mean that the possible changes that the method could make are more limited, while fewer assertions means that more changes are allowed.
As an example, suppose the method has an argument int[] A. If the requires clause that says "A is sorted" (meaning A[0] is the smallest, A[1] is the next smalles, etc.), then you have complete information about how the array will be changed. If the requires clause says that "A[0] is the smallest", then you know what will be in A[0] when the method exits but know nothing about how the rest of the array may be changed. Finally, if the requires class says nothing about A, then it may be changed arbitrarily.
An error condition should either be removed by the precondition using "requires" or given as the condition for an exception using "throws" but never both.
Assertions listed in "requires" are preconditions. They say that the method makes no promises about what it will do if the condition does not hold. In contrast, conditions listed in "throws" are actually postconditions: they are promises to produce output via an exception in those cases.
Listing a condition in "throws" and then excluding it via "requires" is contradictory. The latter says, "I make no promises what I will do if X does not hold", while the former says, "I promise to throw exception Y when X does not hold." You can either make no promises about what happens when X does not hold or you can promise to throw an exception when X it does not hold, but you can't do both.