001: // @(#)$Id: JMLInfiniteIntegerClass.java 1.1 Mon, 02 May 2005 14:31:03 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999 Iowa State University
004:
005: // This file is part of JML
006:
007: // JML is free software; you can redistribute it and/or modify
008: // it under the terms of the GNU General Public License as published by
009: // the Free Software Foundation; either version 2, or (at your option)
010: // any later version.
011:
012: // JML is distributed in the hope that it will be useful,
013: // but WITHOUT ANY WARRANTY; without even the implied warranty of
014: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
015: // GNU General Public License for more details.
016:
017: // You should have received a copy of the GNU General Public License
018: // along with JML; see the file COPYING. If not, write to
019: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
020:
021: package org.jmlspecs.models;
022:
023: import java.math.BigInteger;
024:
025: /** Class with common code to implement JMLInfiniteInteger.
026: *
027: * @version $Revision: 1.1 $
028: * @author Gary T. Leavens
029: * @see java.math.BigInteger
030: */
031: //-@ immutable
032: public abstract/*@ pure @*/class JMLInfiniteIntegerClass implements
033: JMLInfiniteInteger {
034:
035: //@ public invariant owner == null;
036:
037: /** Return a clone of this integer.
038: */
039: public Object clone() {
040: return this ;
041: }
042:
043: /** Tell whether this integer is equal to the argument.
044: ** Note that comparisons to BigIntegers are also handled.
045: */
046: public boolean equals(Object o) {
047: if (o != null) {
048: try {
049: return compareTo(o) == 0;
050: } catch (ClassCastException cce) {
051: return false;
052: }
053: } else {
054: return false;
055: }
056: }
057:
058: /** Compare this to n, returning a comparison code.
059: * @param n the object this is compared to.
060: */
061: public abstract int compareTo(/*@ non_null @*/JMLInfiniteInteger n);
062:
063: /** Tell if this integer is greater than or equal to the argument.
064: */
065: public boolean greaterThanOrEqualTo(JMLInfiniteInteger n) {
066: return compareTo(n) >= 0;
067: }
068:
069: /** Tell if this integer is less than or equal to the argument.
070: */
071: public boolean lessThanOrEqualTo(JMLInfiniteInteger n) {
072: return compareTo(n) <= 0;
073: }
074:
075: /** Tell if this integer is strictly greater than the argument.
076: */
077: public boolean greaterThan(JMLInfiniteInteger n) {
078: return compareTo(n) > 0;
079: }
080:
081: /** Tell if this integer is strictly less than the argument.
082: */
083: public boolean lessThan(JMLInfiniteInteger n) {
084: return compareTo(n) < 0;
085: }
086:
087: /** Return the absolute value of this integer.
088: */
089: public JMLInfiniteInteger abs() {
090: if (signum() >= 0) {
091: return this ;
092: } else {
093: return this .negate();
094: }
095: }
096:
097: /** Return the maximum of this integer and the argument.
098: */
099: public JMLInfiniteInteger max(JMLInfiniteInteger n) {
100: if (compareTo(n) >= 0) {
101: return this ;
102: } else {
103: return n;
104: }
105: }
106:
107: public JMLInfiniteInteger min(JMLInfiniteInteger n) {
108: if (compareTo(n) <= 0) {
109: return this;
110: } else {
111: return n;
112: }
113: }
114: }
|