Java Reference
In-Depth Information
If a method has been called in accordance with its preconditions, then it must
ensure that its postconditions are valid.
349
350
Here is a postcondition that makes a statement about the object state after the
deposit
method is called.
/**
Deposits money into this account.
(Postcondition:
getBalance() >= 0)
@param amount
the amount of money to deposit
(Precondition:
amount >= 0)
*/
As long as the precondition is fulfilled, this method guarantees that the balance after
the deposit is not negative.
Some
javadoc
extensions support a
@postcondition
or
@ensures
tag.
However, just as with preconditions, we simply add postconditions to the method
explanation or the
@return
tag, because the standard
javadoc
program skips all
tags that it doesn't know.
Some programmers feel that they must specify a postcondition for every method.
When you use
javadoc
, however, you already specify a part of the postcondition in
the
@return
tag, and you shouldn't repeat it in a postcondition.
// This postcondition statement is overly repetitive.
/**
Returns the current balance of this account.
@return
the account balance
(Postcondition: The return value equals the
account balance
.)
*/
Note that we formulate pre- and postconditions only in terms of the interface of the
class. Thus, we state the precondition of the
withdraw
method as
amount <=
getBalance()
, not
amount<= balance
. After all, the caller, which needs to
check the precondition, has access only to the public interface, not the private
implementation.