001: // @(#)$Id: JMLInteger.java 1.2 Mon, 09 May 2005 15:27:50 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999, 2002 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: /** A reflection of {@link java.lang.Integer} that implements {@link JMLType}.
024: *
025: * @version $Revision: 1.2 $
026: * @author Gary T. Leavens
027: * @author Brandon Shilling
028: * @see java.lang.Integer
029: * @see JMLLong
030: * @see JMLShort
031: * @see JMLByte
032: * @see JMLChar
033: * @see JMLType
034: */
035: //-@ immutable
036: public/*@ pure @*/class JMLInteger implements JMLComparable {
037:
038: /** The integer value of this object. */
039: //@ public model int theInt;
040: //@ public constraint theInt == \old(theInt);
041: private int intValue;
042:
043: //@ in theInt;
044: //@ private represents theInt <- intValue;
045:
046: //@ public invariant owner == null;
047:
048: /** Initialize this object to 0.
049: */
050: /*@ public normal_behavior
051: @ assignable theInt, owner;
052: @ ensures theInt == 0;
053: @*/
054: public JMLInteger() {
055: intValue = 0;
056: }
057:
058: /** Initialize this object to the given int.
059: */
060: /*@ public normal_behavior
061: @ assignable theInt, owner;
062: @ ensures theInt == inInt;
063: @*/
064: public JMLInteger(int inInt) {
065: intValue = inInt;
066: }
067:
068: /** Initialize this object to the given Integer's value.
069: * @param inInteger an object containing the value to use.
070: */
071: /*@ public normal_behavior
072: @ requires inInteger != null;
073: @ assignable theInt, owner;
074: @ ensures theInt == inInteger.intValue();
075: @*/
076: public JMLInteger(/*@ non_null */Integer inInteger) {
077: intValue = inInteger.intValue();
078: }
079:
080: /** Initialize this object to the given integer.
081: * @param s a string that contains the decimal representation of
082: * the desired value.
083: */
084: /*@ public behavior
085: @ requires s != null
086: @ && (* s is a properly formatted int literal *);
087: @ assignable theInt, owner;
088: @ ensures theInt == (new Integer(s)).intValue();
089: @*/
090: public JMLInteger(/*@ non_null @*/String s)
091: throws JMLTypeException {
092: try {
093: intValue = Integer.valueOf(s).intValue();
094: } catch (RuntimeException re) {
095: throw new JMLTypeException("Bad format string passed to "
096: + "JMLInteger(String): \"" + s + "\"");
097: }
098: }
099:
100: /** The JMLInteger that represents zero.
101: */
102: public static final JMLInteger ZERO = new JMLInteger();
103:
104: /** The JMLInteger that represents one.
105: */
106: public static final JMLInteger ONE = new JMLInteger(1);
107:
108: /** Return a clone of this object.
109: */
110: /*@ also
111: @ public normal_behavior
112: @ ensures \result instanceof JMLInteger
113: @ && ((JMLInteger)\result).theInt == theInt;
114: @*/
115: public Object clone() {
116: return this ;
117: }
118:
119: /** Compare this to op2, returning a comparison code.
120: * @param op2 the object this is compared to.
121: * @exception ClassCastException when o is not a JMLInteger.
122: */
123: /*@ also
124: @ public normal_behavior
125: @ requires op2 instanceof JMLInteger;
126: @ ensures (theInt < ((JMLInteger)op2).theInt ==> \result == -1)
127: @ && (theInt == ((JMLInteger)op2).theInt ==> \result == 0)
128: @ && (theInt > ((JMLInteger)op2).theInt ==> \result == +1);
129: @ also
130: @ public exceptional_behavior
131: @ requires !(op2 instanceof JMLInteger);
132: @ signals (ClassCastException);
133: @*/
134: public int compareTo(Object op2) throws ClassCastException {
135: if (op2 instanceof JMLInteger) {
136: int iv2 = ((JMLInteger) op2).intValue;
137: if (intValue < iv2) {
138: return -1;
139: } else if (intValue == iv2) {
140: return 0;
141: } else {
142: return +1;
143: }
144: } else {
145: throw new ClassCastException();
146: }
147: }
148:
149: /** Test whether this object's value is equal to the given argument.
150: */
151: /*@ also
152: @ public normal_behavior
153: @ ensures \result <==> op2 != null && op2 instanceof JMLInteger
154: @ && theInt == ((JMLInteger)op2).theInt;
155: @*/
156: public boolean equals(Object op2) {
157: return op2 != null && op2 instanceof JMLInteger
158: && intValue == ((JMLInteger) op2).intValue;
159: }
160:
161: /** Return a hash code for this object.
162: */
163: public/*@ pure @*/int hashCode() {
164: return intValue;
165: }
166:
167: /** Return the integer value in this object.
168: */
169: /*@ public normal_behavior
170: @ ensures \result == theInt;
171: @*/
172: public int intValue() {
173: return intValue;
174: }
175:
176: /** Return an Integer object containing the integer value in this
177: * object.
178: */
179: /*@ public normal_behavior
180: @ ensures \result != null && \result.equals(new Integer(theInt));
181: @*/
182: public/*@ non_null @*/Integer getInteger() {
183: return new Integer(intValue);
184: }
185:
186: /** Return a new object containing the negation of this object's
187: * integer value.
188: */
189: /*@ public normal_behavior
190: @ ensures \result != null && \result.theInt == \nowarn_op(- theInt);
191: @*/
192: public/*@ non_null @*/JMLInteger negated() {
193: return new JMLInteger(-intValue);
194: }
195:
196: /** Return a new object containing the sum of this object's
197: * integer value and that of the given argument.
198: */
199: /*@ public normal_behavior
200: @ requires i2 != null;
201: @ ensures \result != null
202: @ && \result.theInt == \nowarn_op(theInt + i2.theInt);
203: @*/
204: public/*@ non_null @*/JMLInteger plus(
205: /*@ non_null @*/JMLInteger i2) {
206: return new JMLInteger(intValue + i2.intValue);
207: }
208:
209: /** Return a new object containing the difference between this object's
210: * integer value and that of the given argument.
211: */
212: /*@ public normal_behavior
213: @ requires i2 != null;
214: @ ensures \result != null
215: @ && \result.theInt == \nowarn_op(theInt - i2.theInt);
216: @*/
217: public/*@ non_null @*/JMLInteger minus(
218: /*@ non_null @*/JMLInteger i2) {
219: return new JMLInteger(intValue - i2.intValue);
220: }
221:
222: /** Return a new object containing the product of this object's
223: * integer value and that of the given argument.
224: */
225: /*@ public normal_behavior
226: @ requires i2 != null;
227: @ ensures \result != null
228: @ && \result.theInt == \nowarn_op(theInt * i2.theInt);
229: @*/
230: public/*@ non_null @*/JMLInteger times(
231: /*@ non_null @*/JMLInteger i2) {
232: return new JMLInteger(intValue * i2.intValue);
233: }
234:
235: /** Return a new object containing the quotient of this object's
236: * integer value divided by that of the given argument.
237: */
238: /*@ public normal_behavior
239: @ requires i2 != null && !i2.equals(new JMLInteger(0));
240: @ ensures \result != null
241: @ && \result.theInt == \nowarn_op(theInt / i2.theInt);
242: @*/
243: public/*@ non_null @*/
244: JMLInteger dividedBy(/*@ non_null @*/JMLInteger i2) {
245: return new JMLInteger(intValue / i2.intValue);
246: }
247:
248: /** Return a new object containing the remainder of this object's
249: * integer value divided by that of the given argument.
250: */
251: /*@ public normal_behavior
252: @ requires i2 != null && !i2.equals(new JMLInteger(0));
253: @ ensures \result != null
254: @ && \result.theInt == theInt % i2.theInt;
255: @*/
256: public/*@ non_null @*/
257: JMLInteger remainderBy(/*@ non_null @*/JMLInteger i2) {
258: return new JMLInteger(intValue % i2.intValue);
259: }
260:
261: /** Tell whether this object's integer value is strictly greater
262: * than that of the given argument.
263: */
264: /*@ public normal_behavior
265: @ requires i2 != null;
266: @ ensures \result <==> theInt > i2.theInt;
267: @*/
268: public boolean greaterThan(/*@ non_null */JMLInteger i2) {
269: return intValue > i2.intValue;
270: }
271:
272: /** Tell whether this object's integer value is strictly less
273: * than that of the given argument.
274: */
275: /*@ public normal_behavior
276: @ requires i2 != null;
277: @ ensures \result <==> theInt < i2.theInt;
278: @*/
279: public boolean lessThan(/*@ non_null */JMLInteger i2) {
280: return intValue < i2.intValue;
281: }
282:
283: /** Tell whether this object's integer value is greater than or equal
284: * to that of the given argument.
285: */
286: /*@ public normal_behavior
287: @ requires i2 != null;
288: @ ensures \result <==> theInt >= i2.theInt;
289: @*/
290: public boolean greaterThanOrEqualTo(/*@ non_null */JMLInteger i2) {
291: return intValue >= i2.intValue;
292: }
293:
294: /** Tell whether this object's integer value is less than or equal
295: * to that of the given argument.
296: */
297: /*@ public normal_behavior
298: @ requires i2 != null;
299: @ ensures \result <==> theInt <= i2.theInt;
300: @*/
301: public boolean lessThanOrEqualTo(/*@ non_null */JMLInteger i2) {
302: return intValue <= i2.intValue;
303: }
304:
305: /** Return a string representation of this object.
306: */
307: /*@ also
308: @ public normal_behavior
309: @ ensures \result != null && \result.equals(getInteger().toString());
310: @*/
311: public String toString() {
312: return String.valueOf(intValue);
313: }
314:
315: }
|