org.jmlspecs.samples.prelimdesign
Interface MoneyComparable

All Superinterfaces:

Cloneable, JMLType, Money, Serializable

All Known Subinterfaces:

MoneyOps

All Known Implementing Classes:

MoneyComparableAC, USMoney

public interface MoneyComparable

extends Money

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

 

Method Summary
boolean	greaterThan(Money m2)
boolean	greaterThanOrEqualTo(Money m2)
boolean	lessThan(Money m2)
boolean	lessThanOrEqualTo(Money m2)

 

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

cents, clone, dollars, equals

 

Methods inherited from interface org.jmlspecs.models.JMLType

hashCode

 

Method Detail

greaterThan

public boolean greaterThan(Money m2)

Specifications: (class)pure

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

greaterThanOrEqualTo

public boolean greaterThanOrEqualTo(Money m2)

Specifications: (class)pure

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

lessThan

public boolean lessThan(Money m2)

Specifications: (class)pure

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

lessThanOrEqualTo

public boolean lessThanOrEqualTo(Money m2)

Specifications: (class)pure

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