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