Java Reference
In-Depth Information
/**
Constructs a bank account with a given balance.
@param initial Balance
the initial balance
(Precondition:
initial Balance >= 0)
*/
public BankAccount(double initialBalance) {. .
.}
{
balance = initialBalance;
}
/**
Deposits money into the bank account.
@param amount
the amount to deposit
(Precondition:
amount >= 0)
*/
public void deposit(double amount) {. . .}
/**
Withdraws money from the bank account.
@param amount
the amount to withdraw
(Precondition:
amount <= getBalance())
*/
public void withdraw(double amount) {. . .}
. . .
}
Now we can formulate the following invariant:
getBalance() >= 0
To see why this invariant is true, first check the constructor; because the
precondition of the constructor is
initialBalance >= 0
we can prove that the invariant is true after the constructor has set
balance
to
initial Balance
.
351
352
Next, check the mutators. The precondition of the
deposit
method is
amount >= 0
We can assume that the invariant condition holds before calling the method. Thus,
we know that
balance >= 0
before the method executes. The laws of
