org.jmlspecs.models.resolve
Interface TotalCompareTo

All Superinterfaces:

CompareTo, ReflexiveCompareTo

All Known Subinterfaces:

StrictlyOrderedCompareTo, TotallyOrderedCompareTo, TotalPreorderedCompareTo, TrichotomousCompareTo

All Known Implementing Classes:

NaturalNumber

public interface TotalCompareTo

extends ReflexiveCompareTo

Objects whose compareTo operation is guaranteed not to throw an UndefinedException and only throws a ClassCastException when the class of the argument prohibits comparison.

Version:

$Revision: 1.10 $

Author:

Gary T. Leavens

Class Specifications

Specifications inherited from class Object

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

Specifications inherited from interface ReflexiveCompareTo

instance public invariant ( \forall org.jmlspecs.models.resolve.ReflexiveCompareTo x; x != null; x.isComparableTo(x)&&x.compareTo(x) == 0);

Model Method Summary
boolean	isComparableTo(Object obj)

 

Method Summary
int	compareTo(non_null Object obj)           Compare this to obj, returning negative if this is strictly less than obj, 0 if they are equal, and positive otherwise.

 

Model Method Detail

isComparableTo

public boolean isComparableTo(Object obj)

Specifications: pure

     also

public model_program { ... }

Specifications inherited from overridden method isComparableTo(Object obj) in interface CompareTo:
       pure

public normal_behavior
ensures \result <==> (* there is a defined comparison between obj and this *);

     also

public model_program { ... }

compareTo

public int compareTo(non_null Object obj)
                       throws ClassCastException,
                              NullPointerException

Description copied from interface: CompareTo

Compare this to obj, returning negative if this is strictly less than obj, 0 if they are equal, and positive otherwise.

Specified by:

compareTo in interface CompareTo

Throws:

ClassCastException

NullPointerException

Specifications: pure

     also

public behavior
requires obj != null;
ensures obj instanceof org.jmlspecs.models.resolve.TotalCompareTo;
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) !(obj instanceof org.jmlspecs.models.resolve.TotalCompareTo);

Specifications inherited from overridden method compareTo(Object obj) in interface CompareTo:
       pure

public behavior
requires obj != null;
ensures this.isComparableTo(obj);
ensures (* returns if this is comparable to obj *);
signals_only org.jmlspecs.models.resolve.UndefinedException, java.lang.ClassCastException;
signals (org.jmlspecs.models.resolve.UndefinedException e) (* no comparison between this and obj is defined *)&&e != null;
signals (java.lang.ClassCastException e) (* obj's type prevents it from being compared to this *)&&e != null;