001: // @(#)$Id: JMLNegativeInfinity.java 1.2 Tue, 17 May 2005 14:57:40 +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: /** Negative Infinity.
026: *
027: * @version $Revision: 1.2 $
028: * @author Gary T. Leavens
029: * @see JMLPositiveInfinity
030: */
031: //-@ immutable
032: public/*@ pure @*/class JMLNegativeInfinity 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 JMLNegativeInfinity() {
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 JMLNegativeInfinity) {
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 JMLNegativeInfinity) {
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.MIN_VALUE;
098: }
099:
100: /** Return positive infinity.
101: */
102: public JMLInfiniteInteger negate() {
103: return new JMLPositiveInfinity();
104: }
105:
106: /** Return the sum of this integer and the argument.
107: */
108: public JMLInfiniteInteger add(JMLInfiniteInteger n) {
109: if (n instanceof JMLPositiveInfinity) {
110: return JMLFiniteInteger.ZERO;
111: } else {
112: return this ;
113: }
114: }
115:
116: /** Return the difference between this integer and the argument.
117: */
118: public JMLInfiniteInteger subtract(JMLInfiniteInteger n) {
119: if (n instanceof JMLNegativeInfinity) {
120: return JMLFiniteInteger.ZERO;
121: } else {
122: return this ;
123: }
124: }
125:
126: /** Return the product of this integer and the argument.
127: */
128: public JMLInfiniteInteger multiply(JMLInfiniteInteger n) {
129: if (n.signum() == 0) {
130: return JMLFiniteInteger.ZERO;
131: } else if (n.signum() == -1) {
132: return new JMLPositiveInfinity();
133: } else {
134: return this ;
135: }
136: }
137:
138: /** Return the quotient of this integer divided by the argument.
139: */
140: public JMLInfiniteInteger divide(JMLInfiniteInteger n)
141: throws ArithmeticException {
142: if (n.signum() == 0) {
143: throw new ArithmeticException("division by zero");
144: } else if (n instanceof JMLNegativeInfinity) {
145: return JMLFiniteInteger.ONE;
146: } else if (n instanceof JMLPositiveInfinity) {
147: return JMLFiniteInteger.ONE.negate();
148: } else if (n.signum() == -1) {
149: return new JMLPositiveInfinity();
150: } else {
151: return this ;
152: }
153: }
154:
155: /** Return the remainder of this integer divided by the argument.
156: */
157: public JMLInfiniteInteger remainder(JMLInfiniteInteger n)
158: throws ArithmeticException {
159: if (n.signum() == 0) {
160: throw new ArithmeticException(
161: "can't take remainder by zero");
162: } else {
163: return JMLFiniteInteger.ZERO;
164: }
165: }
166:
167: /** Return this integer modulo the argument.
168: */
169: public JMLInfiniteInteger mod(JMLInfiniteInteger n)
170: throws ArithmeticException {
171: if (n.signum() <= 0) {
172: throw new ArithmeticException("can't mod by zero"
173: + " or negative number");
174: } else {
175: return JMLFiniteInteger.ZERO;
176: }
177: }
178:
179: /** Return this integer raised to the argument's power.
180: */
181: public JMLInfiniteInteger pow(int n) throws ArithmeticException {
182: if (n < 0) {
183: throw new ArithmeticException();
184: } else if (n == 0) {
185: return JMLFiniteInteger.ONE;
186: } else if (n % 2 == 1) {
187: return this ;
188: } else {
189: return this .negate();
190: }
191: }
192:
193: /** Return this integer approximated by a double.
194: */
195: public double doubleValue() {
196: return Double.NEGATIVE_INFINITY;
197: }
198:
199: /** Return this integer approximated by a float.
200: */
201: public float floatValue() {
202: return Float.NEGATIVE_INFINITY;
203: }
204:
205: /** Return the string "-Infinity".
206: */
207: public String toString() {
208: return "-Infinity";
209: }
210:
211: /** Return the string "-Infinity".
212: */
213: public String toString(int radix) {
214: return toString();
215: }
216: }
|