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