Postconditions

• Condition that is true after a method has completed

• If method call is in accordance with preconditions,
  it must ensure that postconditions are valid

• There are two kinds of postconditions:

  • The return value is computed correctly

  • The object is in a certain state after the method call is completed

/**
   Deposits money into this account.
   (Postcondition: getBalance() >= 0)
   @param amount the amount of money to deposit
   (Precondition: amount >= 0) */

• Don't document trivial postconditions that repeat the @return clause

amount <= getBalance() // this is the way to state a postcondition
amount <= balance // wrong postcondition formulation

• Contract: If caller fulfills precondition, method must fulfill postcondition

Why might you want to add a precondition to a method that you provide for other programmers?

   Answer: Then you don't have to worry about checking for invalid values – it becomes the caller's responsibility.

When you implement a method with a precondition and you notice that the caller did not fulfill the precondition, do you have to notify the caller?

   Answer: No – you can take any action that is convenient for you.