001: // @(#)$Id: JMLFloat.java 1.1 Mon, 02 May 2005 14:31:03 +0200 engelc $
002:
003: // Copyright (C) 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.Float} that implements {@link JMLType}.
024: *
025: * @version $Revision: 1.1 $
026: * @author Brandon Shilling
027: * @author Gary T. Leavens
028: * @author David Cok
029: * @see java.lang.Float
030: * @see JMLDouble
031: */
032: //-@ immutable
033: public/*@ pure @*/strictfp class JMLFloat implements JMLComparable {
034:
035: /** The float that is the abstract value of this object.
036: */
037: //@ model public float theFloat;
038: /*@ spec_public @*/private float floatValue;
039:
040: //@ in theFloat;
041: //@ private represents theFloat <- floatValue;
042:
043: //@ public invariant owner == null;
044:
045: /** Initialize this object to contain zero.
046: */
047: /*@ public normal_behavior
048: @ assignable theFloat,owner;
049: @ ensures theFloat == 0.0f;
050: @*/
051: public JMLFloat() {
052: floatValue = 0.0f;
053: //@ set owner = null;
054: }
055:
056: /** Initialize this object to contain the given float.
057: */
058: /*@ public normal_behavior
059: @ requires !Float.isNaN(inFloat);
060: @ assignable theFloat,owner;
061: @ ensures theFloat == inFloat;
062: @ also
063: @ public normal_behavior
064: @ requires Float.isNaN(inFloat);
065: @ assignable theFloat,owner;
066: @ ensures Float.isNaN(theFloat);
067: @*/
068: public JMLFloat(float inFloat) {
069: floatValue = inFloat;
070: //@ set owner = null;
071: }
072:
073: /** Initialize this object to contain an approximation to the
074: * given integer.
075: */
076: /*@ public normal_behavior
077: @ assignable theFloat,owner;
078: @ ensures theFloat == (float)inInt;
079: @*/
080: public JMLFloat(int inInt) {
081: floatValue = (float) inInt;
082: //@ set owner = null;
083: }
084:
085: /** Initialize this object to contain the value of the given
086: * Float.
087: */
088: /*@ public normal_behavior
089: @ requires inFloat != null && !inFloat.isNaN();
090: @ assignable theFloat,owner;
091: @ ensures theFloat == inFloat.floatValue();
092: @ also
093: @ public normal_behavior
094: @ requires inFloat != null && inFloat.isNaN();
095: @ assignable theFloat,owner;
096: @ ensures Float.isNaN(theFloat);
097: @*/
098: public JMLFloat(/*@ non_null */Float inFloat) {
099: floatValue = inFloat.floatValue();
100: //@ set owner = null;
101: }
102:
103: /** Initialize this object to contain the value given by the
104: * string argument.
105: */
106: /*@ public behavior
107: @ requires s != null;
108: @ assignable theFloat,owner;
109: @ ensures (* s is a parseable string that has the format
110: @ of a floating point literal *)
111: @ && theFloat == new Float(s).floatValue();
112: @ signals (NumberFormatException)
113: @ !(* s is a parseable string that has the format
114: @ of a floating point literal *);
115: @*/
116: public JMLFloat(/*@ non_null @*/String s)
117: throws NumberFormatException {
118: floatValue = new Float(s).floatValue();
119: //@ set owner = null;
120: }
121:
122: /** Tell if this object contains either positive or negative infinity.
123: */
124: /*@ public normal_behavior
125: @ ensures \result <==> (theFloat == Float.POSITIVE_INFINITY)
126: @ || (theFloat == Float.NEGATIVE_INFINITY);
127: @*/
128: public boolean isInfinite() {
129: return (floatValue == Float.POSITIVE_INFINITY)
130: || (floatValue == Float.NEGATIVE_INFINITY);
131: }
132:
133: /** Tell if this object contains NaN (not a number).
134: */
135: /*@ public normal_behavior
136: @ ensures \result <==> (theFloat != theFloat);
137: @*/
138: public boolean isNaN() {
139: return (floatValue != floatValue);
140: }
141:
142: /** Return a clone of this object.
143: */
144: /*@ also
145: @ public normal_behavior
146: @ requires !Float.isNaN(theFloat);
147: @ ensures \result != null && \result instanceof JMLFloat
148: @ && ((JMLFloat)\result).theFloat == theFloat;
149: @ also
150: @ public normal_behavior
151: @ requires Float.isNaN(theFloat);
152: @ ensures \result != null && \result instanceof JMLFloat
153: @ && ((JMLFloat)\result).isNaN();
154: @*/
155: public Object clone() {
156: return this ;
157: }
158:
159: /** Compare this to op2, returning a comparison code.
160: * @param op2 the object this is compared to.
161: * @exception ClassCastException when o is not a JMLFloat.
162: */
163: public int compareTo(Object op2) throws ClassCastException {
164: return new Float(floatValue).compareTo(new Float(
165: ((JMLFloat) op2) //@ nowarn Cast;
166: .floatValue));
167: }
168:
169: /** Tell if the argument is zero (either positive or negative).
170: */
171: /*@ public normal_behavior
172: @ ensures \result <==> (f == +0.0f || f == -0.0f);
173: @*/
174: public static/*@ pure @*/boolean isZero(float f) {
175: return f == +0.0f || f == -0.0f;
176: }
177:
178: /** Tell if this object contains zero (either positive or negative).
179: */
180: /*@ public normal_behavior
181: @ ensures \result <==> (theFloat == +0.0f || theFloat == -0.0f);
182: @*/
183: public boolean isZero() {
184: return floatValue == +0.0f || floatValue == -0.0f;
185: }
186:
187: /** Tell whether this object is equal to the argument.
188: */
189: /*@ also
190: @ public normal_behavior
191: @ requires (op2 instanceof JMLFloat) && op2 != null;
192: @ {|
193: @ requires !Float.isNaN(theFloat) && !isZero();
194: @ ensures \result <==> theFloat == ((JMLFloat)op2).theFloat;
195: @ also
196: @ requires Float.isNaN(theFloat);
197: @ ensures \result <==> Float.isNaN(((JMLFloat)op2).theFloat);
198: @ also
199: @ requires isZero();
200: @ ensures \result <==> ((JMLFloat)op2).isZero();
201: @ |}
202: @ also
203: @ public normal_behavior
204: @ requires !(op2 instanceof JMLFloat) || op2 == null;
205: @ ensures \result <==> false;
206: @*/
207: public boolean equals(Object op2) {
208: if (!(op2 instanceof JMLFloat) || op2 == null) {
209: return false;
210: }
211: JMLFloat jmlf2 = (JMLFloat) op2;
212: float fv2 = jmlf2.floatValue;
213: if (Float.isNaN(floatValue) && Float.isNaN(fv2)) {
214: return true;
215: } else if (isZero() && jmlf2.isZero()) {
216: return true;
217: } else {
218: return floatValue == fv2;
219: }
220: }
221:
222: /** Return a hash code for this object.
223: */
224: public int hashCode() {
225: return new Float(floatValue).hashCode();
226: }
227:
228: /** Return the float contained in this object.
229: */
230: /*@ public normal_behavior
231: @ requires !isNaN();
232: @ ensures \result == floatValue;
233: @ also
234: @ requires isNaN();
235: @ ensures Float.isNaN(\result);
236: @*/
237: public float floatValue() {
238: return floatValue;
239: }
240:
241: /** Return a Float containing the float contained in this object.
242: */
243: /*@ public normal_behavior
244: @ ensures \result != null;
245: @ ensures !isNaN() ==> theFloat == \result.floatValue();
246: @ ensures isNaN() ==> \result.isNaN();
247: @*/
248: public/*@ non_null @*/Float getFloat() {
249: return new Float(floatValue);
250: }
251:
252: /** Return the negation of this.
253: */
254: /*@ public normal_behavior
255: @ ensures \result != null;
256: @ ensures \result.equals(new JMLFloat(\nowarn(- theFloat)));
257: @*/
258: public/*@ non_null @*/JMLFloat negated() {
259: return new JMLFloat(-floatValue);
260: }
261:
262: /** Return the sum of this and the given argument.
263: */
264: /*@ public normal_behavior
265: @ requires f2 != null;
266: @ ensures \result != null;
267: @ ensures \result.equals(new JMLFloat(\nowarn(theFloat + f2.theFloat)));
268: @*/
269: public/*@ non_null @*/JMLFloat plus(/*@ non_null */JMLFloat f2) {
270: return new JMLFloat(floatValue + f2.floatValue());
271: }
272:
273: /** Return the difference between this and the given argument.
274: */
275: /*@ public normal_behavior
276: @ requires f2 != null;
277: @ ensures \result != null;
278: @ ensures \result.equals(new JMLFloat(\nowarn(theFloat - f2.theFloat)));
279: @*/
280: public/*@ non_null @*/JMLFloat minus(/*@ non_null */JMLFloat f2) {
281: return new JMLFloat(floatValue - f2.floatValue());
282: }
283:
284: /** Return the product of this and the given argument.
285: */
286: /*@ public normal_behavior
287: @ requires f2 != null;
288: @ ensures \result != null
289: @ && \result.equals(new JMLFloat(\nowarn(theFloat * f2.theFloat)));
290: @ implies_that
291: @ public normal_behavior
292: @ requires f2 != null;
293: @ requires f2.isNaN()
294: @ || (this.isZero() && f2.isInfinite())
295: @ || (f2.isZero() && this.isInfinite());
296: @ ensures \result != null && \result.isNaN();
297: @*/
298: public/*@ non_null @*/JMLFloat times(/*@ non_null */JMLFloat f2) {
299: return new JMLFloat(floatValue * f2.floatValue());
300: }
301:
302: /** Return the quotient of this divided by the given argument.
303: */
304: /*@ public normal_behavior
305: @ requires f2 != null;
306: @ ensures \result != null
307: @ && \result.equals(new JMLFloat(\nowarn(theFloat / f2.theFloat)));
308: @ implies_that
309: @ public normal_behavior
310: @ requires f2 != null;
311: @ requires f2.isZero() || f2.isNaN();
312: @ ensures \result != null && \result.isNaN();
313: @*/
314: public/*@ non_null @*/
315: JMLFloat dividedBy(/*@ non_null */JMLFloat f2) {
316: return new JMLFloat(floatValue / f2.floatValue());
317: }
318:
319: /** Return the remainder of this divided by the given argument.
320: */
321: /*@ public normal_behavior
322: @ requires f2 != null;
323: @ ensures \result != null
324: @ && \result.equals(new JMLFloat(theFloat % f2.theFloat));
325: @ implies_that
326: @ public normal_behavior
327: @ requires f2 != null;
328: @ requires f2.isZero() || f2.isNaN();
329: @ ensures \result != null && \result.isNaN();
330: @*/
331: public/*@ non_null @*/
332: JMLFloat remainderBy(/*@ non_null @*/JMLFloat f2) {
333: return new JMLFloat(floatValue % f2.floatValue());
334: }
335:
336: /** Tell whether this is strictly greater than the given argument.
337: */
338: /*@ public normal_behavior
339: @ requires f2 != null;
340: @ ensures \result <==> this.theFloat > f2.theFloat;
341: @*/
342: public boolean greaterThan(/*@ non_null */JMLFloat f2) {
343: return (floatValue > f2.floatValue());
344: }
345:
346: /** Tell whether this is strictly less than the given argument.
347: */
348: /*@ public normal_behavior
349: @ requires f2 != null;
350: @ ensures \result <==> this.theFloat < f2.theFloat;
351: @*/
352: public boolean lessThan(/*@ non_null */JMLFloat f2) {
353: return (floatValue < f2.floatValue());
354: }
355:
356: /** Tell whether this is greater than or equal to the given argument.
357: */
358: /*@ public normal_behavior
359: @ requires f2 != null;
360: @ ensures \result <==> this.theFloat >= f2.theFloat;
361: @*/
362: public boolean greaterThanOrEqualTo(/*@ non_null */JMLFloat f2) {
363: return (floatValue >= f2.floatValue());
364: }
365:
366: /** Tell whether this is less than or equal to the given argument.
367: */
368: /*@ public normal_behavior
369: @ requires f2 != null;
370: @ ensures \result <==> this.theFloat <= f2.theFloat;
371: @*/
372: public boolean lessThanOrEqualTo(/*@ non_null */JMLFloat f2) {
373: return (floatValue <= f2.floatValue());
374: }
375:
376: /** Return a string representation of this object.
377: */
378: // specification inherited from Object
379: public String toString() {
380: return String.valueOf(floatValue);
381: }
382:
383: /** Tell whether absolute value of difference of this JMLFloat and the arg
384: * is within the given epsilon.
385: */
386: /*@ public normal_behavior
387: @ requires f2 != null;
388: @ assignable \nothing;
389: @ ensures \result <==>
390: @ StrictMath.abs(\nowarn(theFloat - f2.theFloat)) <= epsilon;
391: @*/
392: public boolean withinEpsilonOf(/*@ non_null @*/JMLFloat f2,
393: float epsilon) {
394: return StrictMath.abs(floatValue() - f2.floatValue()) <= epsilon;
395: }
396:
397: /** Tell whether relative difference of this JMLFloat and the arg is
398: * within the given epsilon.
399: * @see #approximatelyEqualTo(float, float, float)
400: */
401: /*@ public normal_behavior
402: @ requires f2 != null;
403: @ assignable \nothing;
404: @ ensures \result
405: @ <==> approximatelyEqualTo(theFloat, f2.theFloat, epsilon);
406: @*/
407: public boolean approximatelyEqualTo(/*@ non_null @*/JMLFloat f2,
408: float epsilon) {
409: return approximatelyEqualTo(floatValue(), f2.floatValue(),
410: epsilon);
411: }
412:
413: /** Tell whether absolute value of difference of this JMLFloat and the arg
414: * is within the given epsilon.
415: */
416: /*@ public normal_behavior
417: @ requires f2 != null;
418: @ assignable \nothing;
419: @ ensures \result <==>
420: @ StrictMath.abs(\nowarn(theFloat - f2.floatValue())) <= epsilon;
421: @*/
422: public boolean withinEpsilonOf(/*@ non_null @*/Float f2,
423: float epsilon) {
424: return StrictMath.abs(floatValue() - f2.floatValue()) <= epsilon;
425: }
426:
427: /** Tell whether relative difference of this JMLFloat and the arg is
428: * within the given epsilon.
429: * @see #approximatelyEqualTo(float, float, float)
430: */
431: /*@ public normal_behavior
432: @ requires f2 != null;
433: @ assignable \nothing;
434: @ ensures \result
435: @ <==> approximatelyEqualTo(theFloat, f2.floatValue(), epsilon);
436: @*/
437: public boolean approximatelyEqualTo(/*@ non_null @*/Float f2,
438: float epsilon) {
439: return approximatelyEqualTo(floatValue(), f2.floatValue(),
440: epsilon);
441: }
442:
443: /** Tell whether absolute value of difference of this JMLFloat and the arg
444: * is within the given epsilon.
445: */
446: /*@ public normal_behavior
447: @ assignable \nothing;
448: @ ensures \result <==>
449: @ StrictMath.abs(\nowarn(theFloat - f2)) <= epsilon;
450: @*/
451: public boolean withinEpsilonOf(float f2, float epsilon) {
452: return StrictMath.abs(floatValue() - f2) <= epsilon;
453: }
454:
455: /** Tell whether relative difference of this JMLFloat and the arg is
456: * within the given epsilon.
457: * @see #approximatelyEqualTo(float, float, float)
458: */
459: /*@ public normal_behavior
460: @ assignable \nothing;
461: @ ensures \result
462: @ <==> approximatelyEqualTo(theFloat, f2, epsilon);
463: @*/
464: public boolean approximatelyEqualTo(float f2, float epsilon) {
465: return approximatelyEqualTo(floatValue(), f2, epsilon);
466: }
467:
468: /** Tell whether absolute value of difference of the two arguments
469: * is within the given epsilon.
470: */
471: /*@ public normal_behavior
472: @ assignable \nothing;
473: @ ensures \result <==>
474: @ StrictMath.abs(\nowarn(f1 - f2)) <= epsilon;
475: @*/
476: public static/*@ pure @*/boolean withinEpsilonOf(float f1,
477: float f2, float epsilon) {
478: return StrictMath.abs(f1 - f2) <= epsilon;
479: }
480:
481: /** Tell whether relative difference of the two arguments is
482: * within the given epsilon.
483: */
484: /*@ public normal_behavior
485: @ assignable \nothing;
486: @ ensures \result <==>
487: @ f1 == f2
488: @ || StrictMath.abs(\nowarn(f1 - f2))
489: @ <= StrictMath.max(StrictMath.abs(f1),
490: @ StrictMath.abs(f2))
491: @ * epsilon;
492: @*/
493: public static/*@ pure @*/boolean approximatelyEqualTo(float f1,
494: float f2, float epsilon) {
495: return f1 == f2
496: || StrictMath.abs(f1 - f2) <= StrictMath.max(StrictMath
497: .abs(f1), StrictMath.abs(f2))
498: * epsilon;
499: }
500:
501: /** Tell whether absolute value of difference of this JMLFloat and the arg
502: * is within the given epsilon.
503: */
504: /*@ public normal_behavior
505: @ requires f1 != null && f2 != null;
506: @ assignable \nothing;
507: @ ensures \result <==>
508: @ StrictMath.abs(\nowarn(f1.theFloat - f2.theFloat)) <= epsilon;
509: @*/
510: public static/*@ pure @*/boolean withinEpsilonOf(
511: /*@ non_null @*/JMLFloat f1,
512: /*@ non_null @*/JMLFloat f2, float epsilon) {
513: return StrictMath.abs(f1.floatValue() - f2.floatValue()) <= epsilon;
514: }
515:
516: /** Tell whether relative difference of this JMLFloat and the arg is
517: * within the given epsilon.
518: * @see #approximatelyEqualTo(float, float, float)
519: */
520: /*@ public normal_behavior
521: @ requires f1 != null && f2 != null;
522: @ assignable \nothing;
523: @ ensures \result
524: @ <==> approximatelyEqualTo(f1.theFloat, f2.theFloat, epsilon);
525: @*/
526: public static/*@ pure @*/boolean approximatelyEqualTo(
527: /*@ non_null @*/JMLFloat f1,
528: /*@ non_null @*/JMLFloat f2, float epsilon) {
529: return approximatelyEqualTo(f1.floatValue(), f2.floatValue(),
530: epsilon);
531: }
532:
533: /** Tell whether absolute value of difference of this JMLFloat and the arg
534: * is within the given epsilon.
535: */
536: /*@ public normal_behavior
537: @ requires f1 != null && f2 != null;
538: @ assignable \nothing;
539: @ ensures \result <==>
540: @ StrictMath.abs(\nowarn(f1.theFloat - f2.floatValue())) <= epsilon;
541: @*/
542: public static/*@ pure @*/boolean withinEpsilonOf(
543: /*@ non_null @*/JMLFloat f1,
544: /*@ non_null @*/Float f2, float epsilon) {
545: return StrictMath.abs(f1.floatValue() - f2.floatValue()) <= epsilon;
546: }
547:
548: /** Tell whether relative difference of this JMLFloat and the arg is
549: * within the given epsilon.
550: * @see #approximatelyEqualTo(float, float, float)
551: */
552: /*@ public normal_behavior
553: @ requires f1 != null && f2 != null;
554: @ assignable \nothing;
555: @ ensures \result
556: @ <==> approximatelyEqualTo(f1.theFloat, f2.floatValue(), epsilon);
557: @*/
558: public static/*@ pure @*/boolean approximatelyEqualTo(
559: /*@ non_null @*/JMLFloat f1,
560: /*@ non_null @*/Float f2, float epsilon) {
561: return approximatelyEqualTo(f1.floatValue(), f2.floatValue(),
562: epsilon);
563: }
564:
565: /** Tell whether absolute value of difference of this JMLFloat and the arg
566: * is within the given epsilon.
567: */
568: /*@ public normal_behavior
569: @ requires f1 != null;
570: @ assignable \nothing;
571: @ ensures \result <==> StrictMath.abs(\nowarn(f1.theFloat - f2)) <= epsilon;
572: @*/
573: public static/*@ pure @*/boolean withinEpsilonOf(
574: /*@ non_null @*/JMLFloat f1, float f2, float epsilon) {
575: return StrictMath.abs(f1.floatValue() - f2) <= epsilon;
576: }
577:
578: /** Tell whether relative difference of this JMLFloat and the arg is
579: * within the given epsilon.
580: * @see #approximatelyEqualTo(float, float, float)
581: */
582: /*@ public normal_behavior
583: @ requires f1 != null;
584: @ assignable \nothing;
585: @ ensures \result
586: @ <==> approximatelyEqualTo(f1.theFloat, f2, epsilon);
587: @*/
588: public static/*@ pure @*/boolean approximatelyEqualTo(
589: /*@ non_null @*/JMLFloat f1, float f2, float epsilon) {
590: return approximatelyEqualTo(f1.floatValue(), f2, epsilon);
591: }
592: }
|