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