org.jmlspecs.models.resolve
Interface AntisymmetricCompareTo

All Superinterfaces:

CompareTo

All Known Subinterfaces:

DenselyOrderedCompareTo, PartiallyOrderedCompareTo, StrictlyOrderedCompareTo, StrictPartiallyOrderedCompareTo, TotallyOrderedCompareTo

All Known Implementing Classes:

NaturalNumber

public interface AntisymmetricCompareTo

extends CompareTo

Objects with an antisymmetric compareTo operation.

Version:

$Revision: 1.6 $

Author:

Gary T. Leavens

Class Specifications

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