org.jmlspecs.models.resolve
Interface CompareTo

All Known Subinterfaces:

AntisymmetricCompareTo, AsymmetricCompareTo, DenselyOrderedCompareTo, PartiallyOrderedCompareTo, PreorderedCompareTo, ReflexiveCompareTo, StrictlyOrderedCompareTo, StrictPartiallyOrderedCompareTo, SymmetricCompareTo, TotalCompareTo, TotallyOrderedCompareTo, TotalPreorderedCompareTo, TransitiveCompareTo, TrichotomousCompareTo

All Known Implementing Classes:

NaturalNumber

public interface CompareTo

Objects with a compareTo operation. Unlike Comparable, this operation is not assumed to be a total order, and may be partial.

Version:

$Revision: 1.13 $

Author:

Gary T. Leavens

See Also:

TotallyOrderedCompareTo

Class Specifications

Specifications inherited from class Object

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

Model Method Summary
boolean	isComparableTo(non_null 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(non_null Object obj)

Specifications: 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 UndefinedException,
                              ClassCastException,
                              NullPointerException

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

Throws:

UndefinedException

ClassCastException

NullPointerException

Specifications: 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;