Java Reference
In-Depth Information
Bertrand Meyer [
1
] compares preconditions and postconditions to contracts. In real
life, contracts spell out the obligations of the contracting parties. For example, your
mechanic may promise to fix the brakes of your car, and you promise in turn to pay a
certain amount of money. If either party breaks the promise, then the other is not
bound by the terms of the contract. In the same fashion, pre- and postconditions are
contractual terms between a method and its caller. The method promises to fulfill the
postcondition for all inputs that fulfill the precondition. The caller promises never to
call the method with illegal inputs. If the caller fulfills its promise and gets a wrong
answer, it can take the method to Ȓprogrammer's courtȓ. If the caller doesn't fulfill its
promise and something terrible happens as a consequence, it has no recourse.
S
ELF
C
HECK
10.
Why might you want to add a precondition to a method that you provide
for other programmers?
11.
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?
350
351
A
DVANCED
T
OPIC
8.2: Class Invariants
Advanced Topic 6.5
introduced the concept of loop invariants. A loop invariant is
established when the loop is first entered, and it is preserved by all loop iterations.
We then know that the loop invariant must be true when the loop exits, and we can
use that information to reason about the correctness of a loop.
Class invariants fulfill a similar purpose. A class invariant is a statement about an
object that is true after every constructor and that is preserved by every mutator
(provided that the caller respects all preconditions). We then know that the class
invariant must always be true, and we can use that information to reason about the
correctness of our program.
Here is a simple example. Consider a
BankAccount
class with the following
preconditions for the constructor and the mutators:
public class BankAccount
{
