StrictlyOrderedCompareTo (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.models.resolve
Interface StrictlyOrderedCompareTo

All Superinterfaces:: AntisymmetricCompareTo, CompareTo, ReflexiveCompareTo, StrictPartiallyOrderedCompareTo, TotalCompareTo, TransitiveCompareTo, TrichotomousCompareTo

public interface StrictlyOrderedCompareTo
extends StrictPartiallyOrderedCompareTo, TrichotomousCompareTo

Objects with a strictly ordered compareTo operation.

Version:: $Revision: 1.5 $
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 TrichotomousCompareTo

instance public invariant ( \forall org.jmlspecs.models.resolve.TrichotomousCompareTo x, y; x != null&&y != null; x.compareTo(y) < 0||x.compareTo(y) == 0||x.compareTo(y) > 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);

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 ReflexiveCompareTo

instance public invariant ( \forall org.jmlspecs.models.resolve.ReflexiveCompareTo x; x != null; x.isComparableTo(x)&&x.compareTo(x) == 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

Method Summary

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

compareTo

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

compareTo