org.jmlspecs.samples.prelimdesign
Interface MoneyOps

All Superinterfaces:

Cloneable, JMLType, Money, MoneyComparable, Serializable

All Known Implementing Classes:

USMoney

public interface MoneyOps

extends MoneyComparable

Class Specifications

Specifications inherited from class Object

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

Specifications inherited from interface Money

instance public constraint this.pennies == \old(this.pennies);

Model Field Summary

 

Model fields inherited from interface org.jmlspecs.samples.prelimdesign.Money

pennies

 

Model Method Summary
boolean	can_add(Money m2)
boolean	can_scaleBy(double factor)
boolean	inRange(double d)

 

Method Summary
MoneyOps	minus(Money m2)
MoneyOps	plus(Money m2)
MoneyOps	scaleBy(double factor)

 

Methods inherited from interface org.jmlspecs.samples.prelimdesign.MoneyComparable

greaterThan, greaterThanOrEqualTo, lessThan, lessThanOrEqualTo

 

Methods inherited from interface org.jmlspecs.samples.prelimdesign.Money

cents, clone, dollars, equals

 

Methods inherited from interface org.jmlspecs.models.JMLType

hashCode

 

Model Method Detail

inRange

public boolean inRange(double d)

Specifications: (class)pure

public normal_behavior
old double epsilon = 1.0;
assignable \nothing;
ensures \result <==> -9.223372036854776E18+epsilon < d&&d < 9.223372036854776E18-epsilon;

can_add

public boolean can_add(Money m2)

Specifications: (class)pure

public normal_behavior
requires m2 != null;
assignable \nothing;
ensures \result <==> this.inRange(this.pennies+m2.pennies);

can_scaleBy

public boolean can_scaleBy(double factor)

Specifications: (class)pure

public normal_behavior
ensures \result <==> this.inRange(factor*this.pennies);

plus

public MoneyOps plus(Money m2)

Specifications: (class)pure

public normal_behavior
old boolean can_add = this.can_add(m2);
requires m2 != null&&can_add;
assignable \nothing;
ensures \result != null&&\result .pennies == this.pennies+m2.pennies;

    for_example

public normal_example
requires this.pennies == 300&&m2.pennies == 400;
assignable \nothing;
ensures \result != null&&\result .pennies == 700;

minus

public MoneyOps minus(Money m2)

Specifications: (class)pure

public normal_behavior
old boolean inRange = this.inRange(this.pennies-m2.pennies);
requires m2 != null&&inRange;
assignable \nothing;
ensures \result != null&&\result .pennies == this.pennies-m2.pennies;

    for_example

public normal_example
requires this.pennies == 400&&m2.pennies == 300;
assignable \nothing;
ensures \result != null&&\result .pennies == 100;

scaleBy

public MoneyOps scaleBy(double factor)

Specifications: (class)pure

public normal_behavior
requires this.can_scaleBy(factor);
assignable \nothing;
ensures \result != null&&\result .pennies == (long)(factor*this.pennies);

    for_example

public normal_example
requires this.pennies == 400&&factor == 1.01;
assignable \nothing;
ensures \result != null&&\result .pennies == 404;