org.jmlspecs.samples.prelimdesign
Class Account

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

Direct Known Subclasses:

PlusAccount

public class Account

extends Object

Class Specifications

protected invariant this.accountOwner_ != null&&this.credit_ != null; protected invariant_redundantly this.credit_.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0)); public invariant this.accountOwner != null&&this.credit != null&&this.credit.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0)); protected constraint_redundantly this.accountOwner_.equals(\old(this.accountOwner_)); public constraint this.accountOwner.equals(\old(this.accountOwner)); protected represents credit <- this.credit_; protected represents accountOwner <- this.accountOwner_;

Specifications inherited from class Object

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

Model Field Summary
String	accountOwner
MoneyOps	credit

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
protected  String	accountOwner_
protected  MoneyOps	credit_

 

Constructor Summary

Account(MoneyOps amt, String own)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
MoneyOps	balance()
void	deposit(MoneyOps amt)
void	payInterest(double rate)
String	toString()
void	withdraw(MoneyOps amt)

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

credit

public MoneyOps credit

Specifications:
datagroup contains: credit_ org.jmlspecs.samples.prelimdesign.PlusAccount.savings org.jmlspecs.samples.prelimdesign.PlusAccount.checking

accountOwner

public String accountOwner

Specifications:
datagroup contains: accountOwner_

credit_

protected MoneyOps credit_

Specifications:
is in groups: credit

accountOwner_

protected String accountOwner_

Specifications:
is in groups: accountOwner

Account

public Account(MoneyOps amt,
               String own)

Specifications:

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

balance

public MoneyOps balance()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result .equals(this.credit);

payInterest

public void payInterest(double rate)

Specifications:

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

    for_example

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

deposit

public void deposit(MoneyOps amt)

Specifications:

public normal_behavior
old boolean can_add = this.credit.can_add(amt);
requires amt != null&&amt.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0))&&can_add;
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(MoneyOps amt)

Specifications:

public normal_behavior
requires amt != null&&(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));

toString

public String toString()

Overrides:

toString in class Object

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;