Source Code Cross Referenced for JMLDouble.java in  » Testing » KeY » org » jmlspecs » models » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » org.jmlspecs.models 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


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:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.