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.
Search WWH ::




Custom Search