org.jmlspecs.samples.prelimdesign
Class BankAccount

java.lang.Object
  org.jmlspecs.samples.prelimdesign.BankAccount

public class BankAccount

extends Object

Class Specifications

public invariant this.credit != null&&this.owner != null&&this.credit.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0)); public constraint this.owner == \old(this.owner);

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
USMoney	credit
String	owner

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

BankAccount(Money amt, String own)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Money	balance()
void	deposit(MoneyComparable amt)
void	payInterest(double rate)
void	withdraw(MoneyComparable amt)

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Model Field Detail

credit

public USMoney credit

owner

public String owner

BankAccount

public BankAccount(Money amt,
                   String own)

Specifications:

public normal_behavior
requires (new org.jmlspecs.samples.prelimdesign.USMoney(1)).lessThanOrEqualTo(amt);
assignable credit, owner;
ensures this.credit.equals(amt)&&this.owner.equals(own);

balance

public Money balance()

Specifications:

public normal_behavior
assignable \nothing;
ensures \result != null&&\result .equals(this.credit);

payInterest

public void payInterest(double rate)

Specifications:

public normal_behavior
requires 0.0 <= rate&&rate <= 1.0;
assignable credit;
ensures this.credit == \old(this.credit).scaleBy(1.0+rate);

    for_example

public normal_example
requires rate == 0.05&&this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(4000));
assignable credit;
ensures this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(4200));

deposit

public void deposit(MoneyComparable amt)

Specifications:

public normal_behavior
requires amt.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0));
assignable credit;
ensures this.credit.equals(\old(this.credit).plus(amt));

    for_example

public normal_example
requires this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40000))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1));
assignable credit;
ensures this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40001));

withdraw

public void withdraw(MoneyComparable amt)

Specifications:

public normal_behavior
requires (new org.jmlspecs.samples.prelimdesign.USMoney(0)).lessThanOrEqualTo(amt)&&amt.lessThanOrEqualTo(this.credit);
assignable credit;
ensures this.credit.equals(\old(this.credit).minus(amt));

    for_example

public normal_example
requires this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40001))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40000));
assignable credit;
ensures this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1));