org.jmlspecs.models.resolve
Interface TransitiveCompareTo

All Superinterfaces:

CompareTo

All Known Subinterfaces:

DenselyOrderedCompareTo, PartiallyOrderedCompareTo, PreorderedCompareTo, StrictlyOrderedCompareTo, StrictPartiallyOrderedCompareTo, TotallyOrderedCompareTo, TotalPreorderedCompareTo

All Known Implementing Classes:

NaturalNumber

public interface TransitiveCompareTo

extends CompareTo

Objects with a transitive compareTo operation.

Version:

$Revision: 1.6 $

Author:

Gary T. Leavens

Class Specifications

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);

Specifications inherited from class Object

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

Model Method Summary

 

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

isComparableTo

 

Method Summary

 

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

compareTo