JML

org.jmlspecs.models.resolve
Interface DenselyOrderedCompareTo

All Superinterfaces:
AntisymmetricCompareTo, CompareTo, StrictPartiallyOrderedCompareTo, TransitiveCompareTo

public interface DenselyOrderedCompareTo
extends StrictPartiallyOrderedCompareTo

Objects with a dense order for their compareTo operation.

Version:
$Revision: 1.6 $
Author:
Gary T. Leavens

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

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

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

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

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
 


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.