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