001: /* Comparable.java -- Interface for comparaing objects to obtain an ordering
002: Copyright (C) 1998, 1999, 2001, 2002 Free Software Foundation, Inc.
003:
004: This file is part of GNU Classpath.
005:
006: GNU Classpath is free software; you can redistribute it and/or modify
007: it under the terms of the GNU General Public License as published by
008: the Free Software Foundation; either version 2, or (at your option)
009: any later version.
010:
011: GNU Classpath is distributed in the hope that it will be useful, but
012: WITHOUT ANY WARRANTY; without even the implied warranty of
013: MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
014: General Public License for more details.
015:
016: You should have received a copy of the GNU General Public License
017: along with GNU Classpath; see the file COPYING. If not, write to the
018: Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
019: 02111-1307 USA.
020:
021: Linking this library statically or dynamically with other modules is
022: making a combined work based on this library. Thus, the terms and
023: conditions of the GNU General Public License cover the whole
024: combination.
025:
026: As a special exception, the copyright holders of this library give you
027: permission to link this library with independent modules to produce an
028: executable, regardless of the license terms of these independent
029: modules, and to copy and distribute the resulting executable under
030: terms of your choice, provided that you also meet, for each linked
031: independent module, the terms and conditions of the license of that
032: module. An independent module is a module which is not derived from
033: or based on this library. If you modify this library, you may extend
034: this exception to your version of the library, but you are not
035: obligated to do so. If you do not wish to do so, delete this
036: exception statement from your version. */
037:
038: package java.lang;
039:
040: /**
041: * Interface for objects that can be ordering among other objects. The
042: * ordering can be <em>total</em>, such that two objects only compare equal
043: * if they are also equal by the equals method, or <em>partial</em> such
044: * that this is not necessarily true. For example, a case-sensitive
045: * dictionary order comparison of Strings is total, but if it is
046: * case-insensitive it is partial, because "abc" and "ABC" compare as
047: * equal even though "abc".equals("ABC") returns false. However, if you use
048: * a partial ordering, it is a good idea to document your class as
049: * "inconsistent with equals", because the behavior of your class in a
050: * SortedMap will be different than in a HashMap.
051: *
052: * <p>Lists, arrays, and sets of objects that implement this interface can
053: * be sorted automatically, without the need for an explicit
054: * {@link java.util.Comparator}. Note that <code>e1.compareTo(null)</code>
055: * should throw an Exception; as should comparison between incompatible
056: * classes.
057: *
058: * @author Geoff Berry
059: * @author Warren Levy <warrenl@cygnus.com>
060: * @see java.util.Comparator
061: * @see java.util.Collections#sort(java.util.List)
062: * @see java.util.Arrays#sort(Object[])
063: * @see java.util.SortedSet
064: * @see java.util.SortedMap
065: * @see java.util.TreeSet
066: * @see java.util.TreeMap
067: * @since 1.2
068: * @status updated to 1.4
069: */
070: public interface Comparable {
071:
072: /*@ public normal_behavior
073: @ requires i < 0;
074: @ ensures \result == -1;
075: @ also
076: @ public normal_behavior
077: @ requires i == 0;
078: @ ensures \result == 0;
079: @ also
080: @ public normal_behavior
081: @ requires i >= 0;
082: @ ensures \result == +1;
083: @ model pure int sgn(int i);
084: @*/
085:
086: /*@ requires true;
087: model pure boolean definedComparison(non_null Comparable x,
088: non_null Comparable y);
089: @*/
090:
091: /*+@ public instance invariant
092: @ (\forall int n; n == -1 || n == 1;
093: @ (\forall Comparable x, y, z;
094: @ x != null && y != null && z != null
095: @ && definedComparison(x, y) && definedComparison(y, z)
096: @ && definedComparison(x, z);
097: @ sgn(x.compareTo(y)) == n && sgn(y.compareTo(z)) == n
098: @ ==> sgn(x.compareTo(z)) == n));
099: @ public instance invariant
100: @ (\forall int n; n == -1 || n == 1;
101: @ (\forall Comparable x, y, z;
102: @ x != null && y != null && z != null
103: @ && definedComparison(x, y) && definedComparison(y, z)
104: @ && definedComparison(x, z);
105: @ (sgn(x.compareTo(y)) == 0 && sgn(y.compareTo(z)) == n
106: @ || sgn(x.compareTo(y)) == n && sgn(y.compareTo(z)) == 0)
107: @ ==> sgn(x.compareTo(z)) == n));
108: @*/
109:
110: // compareTo returning 0 means the other argument
111: // is in the same equivalence class
112: /*+@ public instance invariant
113: @ (\forall Comparable x, y, z;
114: @ x != null && y != null && z != null
115: @ && definedComparison(x, y) && definedComparison(x, z)
116: @ && definedComparison(y, x);
117: @ sgn(x.compareTo(y)) == 0
118: @ ==> sgn(x.compareTo(z)) == sgn(y.compareTo(x)));
119: @*/
120:
121: // compareTo is reflexive
122: /*+@ public instance invariant
123: @ (\forall Comparable x; x != null; x.compareTo(x) == 0);
124: @*/
125:
126: // compareTo is antisymmetric
127: /*+@ public instance invariant
128: @ (\forall Comparable x, y; x != null && y != null
129: @ && definedComparison(x, y)
130: @ && definedComparison(y, x);
131: @ sgn(x.compareTo(y)) == -sgn(y.compareTo(x)) );
132: @*/
133:
134: /**
135: * Compares this object with another, and returns a numerical result based
136: * on the comparison. If the result is negative, this object sorts less
137: * than the other; if 0, the two are equal, and if positive, this object
138: * sorts greater than the other. To translate this into boolean, simply
139: * perform <code>o1.compareTo(o2) <em><op></em> 0</code>, where op
140: * is one of <, <=, =, !=, >, or >=.
141: *
142: * <p>You must make sure that the comparison is mutual, ie.
143: * <code>sgn(x.compareTo(y)) == -sgn(y.compareTo(x))</code> (where sgn() is
144: * defined as -1, 0, or 1 based on the sign). This includes throwing an
145: * exception in either direction if the two are not comparable; hence,
146: * <code>compareTo(null)</code> should always throw an Exception.
147: *
148: * <p>You should also ensure transitivity, in two forms:
149: * <code>x.compareTo(y) > 0 && y.compareTo(z) > 0</code> implies
150: * <code>x.compareTo(z) > 0</code>; and <code>x.compareTo(y) == 0</code>
151: * implies <code>x.compareTo(z) == y.compareTo(z)</code>.
152: *
153: * @param o the object to be compared
154: * @return an integer describing the comparison
155: * @throws NullPointerException if o is null
156: * @throws ClassCastException if o cannot be compared
157: */
158: /*@
159: @ public behavior
160: @ requires o != null && o instanceof Comparable;
161: @ ensures \result==0 <==> this.equals(o);
162: @*/
163: int compareTo(Object o);
164:
165: }
|