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