JML

java.lang
Interface Comparable

All Known Subinterfaces:
CompilerPassEnterable, JClassDeclarationType, JCompilationUnitType, JConstructorDeclarationType, JInterfaceDeclarationType, JMethodDeclarationType, JMLComparable, JMLInfiniteInteger, JTypeDeclarationType, TotallyOrderedCompareTo
All Known Implementing Classes:
BigDecimal, BigInteger, Byte, CClass, Character, ClassConstant, CMethod, CType, Date, Double, File, Float, InnerClassInfo, Integer, JClassDeclaration, JCompilationUnit, JConstructorDeclaration, JInterfaceDeclaration, JMethodDeclaration, JMLByte, JMLChar, JmlClassDeclaration, JmlCompilationUnit, JmlConstructorDeclaration, JMLDouble, JMLFloat, JmlHTML.IntPair, JmlHTML.IntString, JMLInfiniteIntegerClass, JMLInteger, JmlInterfaceDeclaration, JMLLong, JmlMethodDeclaration, JMLShort, JMLString, JmlTypeDeclaration, JTypeDeclaration, JTypeDeclaration.MethodRecord, Long, Main.Task, Member, NaturalNumber, RacParser.RacMethodDeclaration, Short, String, URI

public interface Comparable

JML's specification of java.lang.Comparable. These are objects with a total ordering that is an equivalence relation.

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

Class Specifications
instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0);
instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x)));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

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

Model Method Summary
 boolean definedComparison(non_null Comparable x, non_null Comparable y)
           
 int sgn(int i)
           
 
Method Summary
 int compareTo(non_null Object o)
           
 

Model Method Detail

sgn

public int sgn(int i)
Specifications: pure
public normal_behavior
requires i < 0;
ensures \result == -1;
     also
public normal_behavior
requires i == 0;
ensures \result == 0;
     also
public normal_behavior
requires i >= 0;
ensures \result == 1;
    implies_that
public model_program { ... }

definedComparison

public boolean definedComparison(non_null Comparable x,
                                 non_null Comparable y)
Specifications: pure
public model_program { ... }
     also
public normal_behavior
ensures \result == this.definedComparison(y,x);
Method Detail

compareTo

public int compareTo(non_null Object o)
Specifications: pure
public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
     also
public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

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.