java.lang
Interface Comparable

All Known Subinterfaces:

CompilerPassEnterable, JClassDeclarationType, JCompilationUnitType, JConstructorDeclarationType, JInterfaceDeclarationType, JMethodDeclarationType, JMLComparable, JMLInfiniteInteger, JTypeDeclarationType, TotallyOrderedCompareTo

All Known Implementing Classes:

BigDecimal, BigInteger, Byte, CClass, Character, ClassConstant, CMethod, CType, Date, Double, File, Float, InnerClassInfo, Integer, JClassDeclaration, JCompilationUnit, JConstructorDeclaration, JInterfaceDeclaration, JMethodDeclaration, JMLByte, JMLChar, JmlClassDeclaration, JmlCompilationUnit, JmlConstructorDeclaration, JMLDouble, JMLFloat, JmlHTML.IntPair, JmlHTML.IntString, JMLInfiniteIntegerClass, JMLInteger, JmlInterfaceDeclaration, JMLLong, JmlMethodDeclaration, JMLShort, JMLString, JmlTypeDeclaration, JTypeDeclaration, JTypeDeclaration.MethodRecord, Long, Main.Task, Member, NaturalNumber, RacParser.RacMethodDeclaration, Short, String, URI

public interface Comparable

JML's specification of java.lang.Comparable. These are objects with a total ordering that is an equivalence relation.

Version:

$Revision: 1.17 $

Author:

Gary T. Leavens

Class Specifications

instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0); instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x))); instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n)); instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n)); instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

Specifications inherited from class Object

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

Model Method Summary
boolean	definedComparison(non_null Comparable x, non_null Comparable y)
int	sgn(int i)

 

Method Summary
int	compareTo(non_null Object o)

 

Model Method Detail

sgn

public int sgn(int i)

Specifications: pure

public normal_behavior
requires i < 0;
ensures \result == -1;

     also

public normal_behavior
requires i == 0;
ensures \result == 0;

     also

public normal_behavior
requires i >= 0;
ensures \result == 1;

    implies_that

public model_program { ... }

definedComparison

public boolean definedComparison(non_null Comparable x,
                                 non_null Comparable y)

Specifications: pure

public model_program { ... }

     also

public normal_behavior
ensures \result == this.definedComparison(y,x);

compareTo

public int compareTo(non_null Object o)

Specifications: pure

public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);

     also

public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);