org.jmlspecs.models.resolve
Interface TotallyOrderedCompareTo

All Superinterfaces:

AntisymmetricCompareTo, Comparable, CompareTo, PreorderedCompareTo, ReflexiveCompareTo, TotalCompareTo, TotalPreorderedCompareTo, TransitiveCompareTo

All Known Implementing Classes:

NaturalNumber

public interface TotallyOrderedCompareTo

extends TotalPreorderedCompareTo, AntisymmetricCompareTo, Comparable

Objects with a totally ordered compareTo operation. This is essentially the same as Java's Comparable interface.

Version:

$Revision: 1.4 $

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 AntisymmetricCompareTo

instance public invariant ( \forall org.jmlspecs.models.resolve.AntisymmetricCompareTo x, y; x != null&&y != null&&x.isComparableTo(y)&&y.isComparableTo(x); x.compareTo(y) <= 0&&y.compareTo(x) <= 0 ==> x.compareTo(y) == 0); instance public invariant_redundantly ( \forall org.jmlspecs.models.resolve.AntisymmetricCompareTo x, y; x != null&&y != null&&x.isComparableTo(y)&&y.isComparableTo(x); x.compareTo(y) >= 0&&y.compareTo(x) >= 0 ==> x.compareTo(y) == 0);

Specifications inherited from interface Comparable

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 interface ReflexiveCompareTo

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

Specifications inherited from interface TransitiveCompareTo

instance public invariant ( \forall org.jmlspecs.models.resolve.TransitiveCompareTo x, y, z; x != null&&y != null&&z != null&&x.isComparableTo(y)&&y.isComparableTo(z); x.compareTo(y) < 0&&y.compareTo(z) < 0 ==> x.isComparableTo(z)&&x.compareTo(z) < 0); instance public invariant ( \forall org.jmlspecs.models.resolve.TransitiveCompareTo x, y, z; x != null&&y != null&&z != null&&x.isComparableTo(y)&&y.isComparableTo(z); x.compareTo(y) <= 0&&y.compareTo(z) <= 0 ==> x.isComparableTo(z)&&x.compareTo(z) <= 0); instance public invariant ( \forall org.jmlspecs.models.resolve.TransitiveCompareTo x, y, z; x != null&&y != null&&z != null&&x.isComparableTo(y)&&y.isComparableTo(z); x.compareTo(y) == 0&&y.compareTo(z) == 0 ==> x.isComparableTo(z)&&x.compareTo(z) == 0); instance public invariant_redundantly ( \forall org.jmlspecs.models.resolve.TransitiveCompareTo x, y, z; x != null&&y != null&&z != null&&x.isComparableTo(y)&&y.isComparableTo(z); x.compareTo(y) >= 0&&y.compareTo(z) >= 0 ==> x.isComparableTo(z)&&x.compareTo(z) >= 0); instance public invariant_redundantly ( \forall org.jmlspecs.models.resolve.TransitiveCompareTo x, y, z; x != null&&y != null&&z != null&&x.isComparableTo(y)&&y.isComparableTo(z); x.compareTo(y) > 0&&y.compareTo(z) > 0 ==> x.isComparableTo(z)&&x.compareTo(z) > 0);

Model Method Summary

 

Model methods inherited from interface org.jmlspecs.models.resolve.CompareTo

isComparableTo

 

Model methods inherited from interface org.jmlspecs.models.resolve.TotalCompareTo

isComparableTo

 

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

 

Method Summary

 

Methods inherited from interface org.jmlspecs.models.resolve.CompareTo

compareTo

 

Methods inherited from interface org.jmlspecs.models.resolve.TotalCompareTo

compareTo

 

Methods inherited from interface java.lang.Comparable

compareTo