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

All Superinterfaces:: CompareTo, PreorderedCompareTo, ReflexiveCompareTo, TotalCompareTo, TransitiveCompareTo

All Known Subinterfaces:: TotallyOrderedCompareTo

All Known Implementing Classes:: NaturalNumber

public interface TotalPreorderedCompareTo
extends PreorderedCompareTo, TotalCompareTo

Objects with a total preorder for their 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 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

Method Summary

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

compareTo

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

compareTo