001: // @(#)$Id: JMLPositiveInfinity.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: /** Positive Infinity.
026: *
027: * @version $Revision: 1.2 $
028: * @author Gary T. Leavens
029: * @see JMLNegativeInfinity
030: */
031: //-@ immutable
032: public/*@ pure @*/class JMLPositiveInfinity extends
033: JMLInfiniteIntegerClass {
034:
035: //@ public represents is_infinite <- true;
036: //@ public represents sign <- +1;
037:
038: //@ public invariant_redundantly is_infinite;
039: //@ public invariant_redundantly sign == +1;
040:
041: //@ public invariant_redundantly nonnegative;
042:
043: /** Initialize this object.
044: */
045: public JMLPositiveInfinity() {
046: }
047:
048: /** Return the sign of this integer.
049: */
050: public int signum() {
051: return +1;
052: }
053:
054: /** Return false.
055: */
056: public boolean isFinite() {
057: return false;
058: }
059:
060: /** Throw an ArithmeticException.
061: */
062: public BigInteger finiteValue() throws ArithmeticException {
063: throw new ArithmeticException();
064: }
065:
066: /** Compare this to the given integer, returning a comparison code.
067: */
068: public int compareTo(JMLInfiniteInteger n) {
069: if (n instanceof JMLPositiveInfinity) {
070: return 0;
071: } else {
072: return +1;
073: }
074: }
075:
076: /** Compare this to o, returning a comparison code.
077: * @param o the object this is compared to.
078: * @exception ClassCastException when o is not
079: * a JMLInfiniteInteger or a BigInteger.
080: */
081: public int compareTo(Object o) throws ClassCastException {
082: if (o == null) {
083: throw new NullPointerException();
084: } else if (o instanceof JMLPositiveInfinity) {
085: return 0;
086: } else if (o instanceof JMLInfiniteInteger
087: || o instanceof BigInteger) {
088: return +1;
089: } else {
090: throw new ClassCastException();
091: }
092: }
093:
094: /** Return a hash code for this object.
095: */
096: public int hashCode() {
097: return Integer.MAX_VALUE;
098: }
099:
100: /** Return negative infinity.
101: */
102: public JMLInfiniteInteger negate() {
103: return new JMLNegativeInfinity();
104: }
105:
106: /** Return the sum of this integer and the argument.
107: */
108: public JMLInfiniteInteger add(JMLInfiniteInteger n) {
109: //@ assume n != null;
110: if (n instanceof JMLNegativeInfinity) {
111: return JMLFiniteInteger.ZERO;
112: } else {
113: return this ;
114: }
115: }
116:
117: /** Return the difference between this integer and the argument.
118: */
119: public JMLInfiniteInteger subtract(JMLInfiniteInteger n) {
120: if (n instanceof JMLPositiveInfinity) {
121: return JMLFiniteInteger.ZERO;
122: } else {
123: return this ;
124: }
125: }
126:
127: /** Return the product of this integer and the argument.
128: */
129: public JMLInfiniteInteger multiply(JMLInfiniteInteger n) {
130: if (n.signum() == 0) {
131: return JMLFiniteInteger.ZERO;
132: } else if (n.signum() == -1) {
133: return new JMLNegativeInfinity();
134: } else {
135: return this ;
136: }
137: }
138:
139: /** Return the quotient of this integer divided by the argument.
140: */
141: public JMLInfiniteInteger divide(JMLInfiniteInteger n)
142: throws ArithmeticException {
143: if (n.signum() == 0) {
144: throw new ArithmeticException("division by zero");
145: } else if (n instanceof JMLPositiveInfinity) {
146: return JMLFiniteInteger.ONE;
147: } else if (n instanceof JMLNegativeInfinity) {
148: return JMLFiniteInteger.ONE.negate();
149: } else if (n.signum() == -1) {
150: return new JMLNegativeInfinity();
151: } else {
152: return this ;
153: }
154: }
155:
156: /** Return the remainder of this integer divided by the argument.
157: */
158: public JMLInfiniteInteger remainder(JMLInfiniteInteger n)
159: throws ArithmeticException {
160: if (n.signum() == 0) {
161: throw new ArithmeticException(
162: "can't take remainder by zero");
163: } else {
164: return JMLFiniteInteger.ZERO;
165: }
166: }
167:
168: /** Return this integer modulo the argument.
169: */
170: public JMLInfiniteInteger mod(JMLInfiniteInteger n)
171: throws ArithmeticException {
172: if (n.signum() <= 0) {
173: throw new ArithmeticException("can't mod by zero"
174: + " or negative number");
175: } else {
176: return JMLFiniteInteger.ZERO;
177: }
178: }
179:
180: /** Return this integer raised to the argument's power.
181: */
182: public JMLInfiniteInteger pow(int n) throws ArithmeticException {
183: if (n < 0) {
184: throw new ArithmeticException();
185: } else if (n == 0) {
186: return JMLFiniteInteger.ONE;
187: } else {
188: return this ;
189: }
190: }
191:
192: /** Return this integer approximated by a double.
193: */
194: public double doubleValue() {
195: return Double.POSITIVE_INFINITY;
196: }
197:
198: /** Return this integer approximated by a float.
199: */
200: public float floatValue() {
201: return Float.POSITIVE_INFINITY;
202: }
203:
204: /** Return the string "Infinity".
205: */
206: public String toString() {
207: return "Infinity";
208: }
209:
210: /** Return the string "Infinity".
211: */
212: public String toString(int radix) {
213: return toString();
214: }
215: }
|