org.jmlspecs.samples.prelimdesign
Class MoneyComparableAC

java.lang.Object
  org.jmlspecs.samples.prelimdesign.MoneyAC
      org.jmlspecs.samples.prelimdesign.MoneyComparableAC

All Implemented Interfaces:

Cloneable, JMLType, Money, MoneyComparable, Serializable

Direct Known Subclasses:

USMoney

public abstract class MoneyComparableAC

extends MoneyAC

implements MoneyComparable

Class Specifications

Specifications inherited from class MoneyAC

protected constraint_redundantly this.numCents == \old(this.numCents); protected represents pennies <- this.numCents;

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 class java.lang.Object

_getClass, objectState, theString

 

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

pennies

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary

 

Fields inherited from class org.jmlspecs.samples.prelimdesign.MoneyAC

numCents

 

Constructor Summary

MoneyComparableAC()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
boolean	greaterThan(Money m2)
boolean	greaterThanOrEqualTo(Money m2)
boolean	lessThan(Money m2)
boolean	lessThanOrEqualTo(Money m2)
protected static long	totalCents(Money m2)

 

Methods inherited from class org.jmlspecs.samples.prelimdesign.MoneyAC

cents, clone, dollars, equals, hashCode

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, toString, wait, wait, wait

 

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

cents, clone, dollars, equals

 

Methods inherited from interface org.jmlspecs.models.JMLType

hashCode

 

Constructor Detail

MoneyComparableAC

public MoneyComparableAC()

totalCents

protected static long totalCents(Money m2)

Specifications: pure

greaterThan

public boolean greaterThan(Money m2)

Specified by:

greaterThan in interface MoneyComparable

Specifications: (class)pure

Specifications inherited from overridden method greaterThan(Money m2) in interface MoneyComparable:
       (class)pure

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

greaterThanOrEqualTo

public boolean greaterThanOrEqualTo(Money m2)

Specified by:

greaterThanOrEqualTo in interface MoneyComparable

Specifications: (class)pure

Specifications inherited from overridden method greaterThanOrEqualTo(Money m2) in interface MoneyComparable:
       (class)pure

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

lessThan

public boolean lessThan(Money m2)

Specified by:

lessThan in interface MoneyComparable

Specifications: (class)pure

Specifications inherited from overridden method lessThan(Money m2) in interface MoneyComparable:
       (class)pure

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

lessThanOrEqualTo

public boolean lessThanOrEqualTo(Money m2)

Specified by:

lessThanOrEqualTo in interface MoneyComparable

Specifications: (class)pure

Specifications inherited from overridden method lessThanOrEqualTo(Money m2) in interface MoneyComparable:
       (class)pure

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