001: // @(#)$Id: JMLFiniteInteger.java 1.2 Mon, 09 May 2005 15:27:50 +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: /** Arbitrary precision integers with a finite value.
026: *
027: * @version $Revision: 1.2 $
028: * @author Gary T. Leavens
029: * @see java.math.BigInteger
030: */
031: //-@ immutable
032: public/*@ pure @*/class JMLFiniteInteger extends
033: JMLInfiniteIntegerClass {
034:
035: protected final/*@ non_null */BigInteger val;
036: //@ in sign, finite_value, is_infinite;
037:
038: //@ protected represents finite_value <- val;
039: //@ protected represents sign <- val.signum();
040: //@ protected represents is_infinite <- false;
041:
042: //@ public invariant !is_infinite;
043:
044: /** The number zero (0).
045: */
046: public static final JMLFiniteInteger ZERO = new JMLFiniteInteger();
047:
048: /** The number one (1).
049: */
050: public static final JMLFiniteInteger ONE = new JMLFiniteInteger(
051: BigInteger.ONE);
052:
053: /** Initialize this finite integer to zero (0).
054: */
055: /*@ public normal_behavior
056: @ assignable nonnegative, sign, is_infinite, finite_value;
057: @ ensures !is_infinite;
058: @ ensures finite_value.equals(BigInteger.ZERO);
059: also private normal_behavior
060: modifies val;
061: @*/
062: public JMLFiniteInteger() {
063: val = BigInteger.ZERO;
064: }
065:
066: /** Initialize this finite integer from the given BigInteger.
067: */
068: /*@ public behavior
069: @ assignable nonnegative, sign, is_infinite, finite_value;
070: @ ensures !is_infinite && finite_value.equals(n);
071: @ signals (IllegalArgumentException) n == null;
072: @*/
073: public JMLFiniteInteger(/*@ non_null @*/BigInteger n)
074: throws IllegalArgumentException {
075: if (n != null) {
076: val = n;
077: } else {
078: throw new IllegalArgumentException();
079: }
080: }
081:
082: /** Initialize this finite integer from the given long.
083: */
084: public JMLFiniteInteger(long n) {
085: val = BigInteger.valueOf(n);
086: }
087:
088: /** Return the sign of this integer.
089: */
090: public int signum() {
091: return val.signum();
092: }
093:
094: /** Return true.
095: */
096: public boolean isFinite() {
097: return true;
098: }
099:
100: /** Return the value of this integer.
101: */
102: public BigInteger finiteValue() {
103: return val;
104: }
105:
106: /** Compare this to the given integer, returning a comparison code.
107: */
108: public int compareTo(JMLInfiniteInteger n) {
109: if (n instanceof JMLFiniteInteger) {
110: return val.compareTo(((JMLFiniteInteger) n).val);
111: } else {
112: return -1 * n.signum();
113: }
114: }
115:
116: /** Compare this to o, returning a comparison code.
117: * @param o the object this is compared to.
118: * @exception ClassCastException when o is not
119: * a JMLInfiniteInteger or a BigInteger.
120: */
121: public int compareTo(Object o) throws ClassCastException {
122: if (o == null) {
123: throw new NullPointerException();
124: } else if (o instanceof BigInteger) {
125: return val.compareTo((BigInteger) o);
126: } else if (o instanceof JMLFiniteInteger) {
127: return val.compareTo(((JMLFiniteInteger) o).val);
128: } else if (o instanceof JMLPositiveInfinity) {
129: return -1;
130: } else if (o instanceof JMLNegativeInfinity) {
131: return +1;
132: } else {
133: throw new ClassCastException();
134: }
135: }
136:
137: /** Return a hash code for this object.
138: */
139: public int hashCode() {
140: return val.hashCode();
141: }
142:
143: /** Return the negation of this integer.
144: */
145: public JMLInfiniteInteger negate() {
146: BigInteger n = val.negate();
147: return new JMLFiniteInteger(n);
148: }
149:
150: /** Return the sum of this integer and the argument.
151: */
152: public JMLInfiniteInteger add(JMLInfiniteInteger n) {
153: if (n instanceof JMLFiniteInteger) {
154: BigInteger s = val.add(((JMLFiniteInteger) n).val);
155: return new JMLFiniteInteger(s);
156: } else {
157: return n;
158: }
159: }
160:
161: /** Return the difference between this integer and the argument.
162: */
163: public JMLInfiniteInteger subtract(JMLInfiniteInteger n) {
164: if (n instanceof JMLFiniteInteger) {
165: BigInteger s = val.subtract(((JMLFiniteInteger) n).val);
166: return new JMLFiniteInteger(s);
167: } else {
168: return n.negate();
169: }
170: }
171:
172: /** Return the product of this integer and the argument.
173: */
174: public JMLInfiniteInteger multiply(JMLInfiniteInteger n) {
175: if (n instanceof JMLFiniteInteger) {
176: BigInteger s = val.multiply(((JMLFiniteInteger) n).val);
177: return new JMLFiniteInteger(s);
178: } else if (val.equals(BigInteger.ZERO)) {
179: return ZERO; //FIXME - ZERO * infinity ????
180: } else if (val.signum() == +1) {
181: return n;
182: } else {
183: JMLInfiniteInteger ret = n.negate();
184: return ret;
185: }
186: }
187:
188: /** Return the quotient of this integer divided by the argument.
189: */
190: public JMLInfiniteInteger divide(JMLInfiniteInteger n) {
191: if (n instanceof JMLFiniteInteger) {
192: BigInteger s = val.divide(((JMLFiniteInteger) n).val);
193: return new JMLFiniteInteger(s);
194: } else {
195: return ZERO;
196: }
197: }
198:
199: /** Return the remainder of this integer divided by the argument.
200: */
201: public JMLInfiniteInteger remainder(JMLInfiniteInteger n) {
202: if (n instanceof JMLFiniteInteger) {
203: BigInteger s = val.remainder(((JMLFiniteInteger) n).val);
204: return new JMLFiniteInteger(s);
205: } else if (n.signum() == +1) {
206: return this ;
207: } else {
208: return this .negate();
209: }
210: }
211:
212: /** Return this integer modulo the argument.
213: */
214: public JMLInfiniteInteger mod(JMLInfiniteInteger n)
215: throws ArithmeticException {
216: if (n instanceof JMLFiniteInteger) {
217: BigInteger s = val.mod(((JMLFiniteInteger) n).val);
218: return new JMLFiniteInteger(s);
219: } else if (n.signum() == +1) {
220: return n;
221: } else {
222: throw new ArithmeticException("negative divisor for mod");
223: }
224: }
225:
226: /** Return this integer raised to the argument's power.
227: */
228: public JMLInfiniteInteger pow(int n) {
229: BigInteger s = val.pow(n);
230: return new JMLFiniteInteger(s);
231: }
232:
233: /** Return this integer approximated by a double.
234: */
235: public double doubleValue() {
236: return val.doubleValue();
237: }
238:
239: /** Return this integer approximated by a float.
240: */
241: public float floatValue() {
242: return val.floatValue();
243: }
244:
245: /** Return the decimal representation of this integer.
246: */
247: public String toString() {
248: return val.toString();
249: }
250:
251: /** Return the digits representing this integer in the given radix.
252: */
253: public String toString(int radix) {
254: return val.toString(radix);
255: }
256:
257: /** Converts this BigInteger to a long
258: */
259: public long longValue() {
260: return val.longValue();
261: }
262:
263: /** Converts this BigInteger to an integer
264: */
265: public int intValue() {
266: return val.intValue();
267: }
268:
269: }
|