Question

Question 2 Programming by Contract (a) Design a BankAccount class for maintaining bank balances. Each bank account should have a current balance and methods implementing deposits and withdrawals; however money can only be withdrawn from an account if there are sufficient funds. Each account has a cash withdrawal limit of $800 per day. Give Java implementations of the methods in your design. Explain how your implementation enforces the daily limit on withdrawals. (b) Give preconditions and postconditions for each method in the BankAccount class and provide a rigorous argument that balance 20 is a class invariant. Explain how your code is consistent with your pre- and postconditions

Answer 1

public class BankAccount

{

public static void main ( String [] args )

{

BankAccount myAccount = new BankAccount( 0.0 );

myAccount.deposit( 500.00 );

System.out.println( "Current balance is " + myAccount.getBalance() );

myAccount.withdraw( 100.00 );

}

/** ********** Implementation starts here ********************* */

/**

* Class Invariant: balance >= 0.0

*/

private double balance = 0.0;

/**

* Create a new bank account object, with some initial balance.

*

* @param amount the amount to initially deposit

* Pre-condition: initialBalance >= 0.0

*/

public BankAccount ( double initialBalance )

{

if ( initialBalance < 0.0 )

throw new IllegalArgumentException( "Initial balance ("

+ initialBalance + ") must be >= 0" );

balance = initialBalance;

assert balance >= 0.0 : "invariant violation: balance = " + balance;

}

/**

* @param amount the amount to deposit

* Pre-condition: amount >= 0.0

*/

public void deposit ( double amount )

{

if ( amount < 0.0 )

throw new IllegalArgumentException( "Deposit amount (" + amount

+ ") must be >= 0" );

double newBalance = balance + amount;

assert newBalance >= balance : "post-condition violation: new balance "

+ "(" + newBalance + ") < current balance (" + balance + ")";

balance = newBalance;

assert balance >= 0.0 : "invariant violation: balance = " + balance;

}

/**

* @param amount the amount to deposit

* Pre-condition: amount >= 0.0

*/

public void withdraw( double amount )

{

if ( amount < 0.0 )

throw new IllegalArgumentException( "Withdraw amount (" + amount

+ ") must be >= 0" );

if ( amount > balance )

throw new IllegalArgumentException( "Withdraw amount (" + amount

+ ") must be <= current balance (" + balance + ")" );

balance -= amount;

assert balance >= 0.0 : "invariant violation: balance = " + balance;

}

/**

* @param amount the amount to deposit

* Pre-condition: amount >= 0.0

*/

public double getBalance ()

{

calculateInterest();

assert balance >= 0.0 : "invariant violation: balance = " + balance;

return balance;

}

/**

* Post-condition: new balance >= old balance

*/

private void calculateInterest ()

{

double newBalance = balance * .05;

assert newBalance >= balance : "post-condition violation: new balance "

+ "(" + newBalance + ") < current balance (" + balance + ")";

balance = newBalance;

assert balance >= 0.0 : "post-condition violation: balance = " + balance;

}

}