001: // @(#)$Id: JMLInfiniteInteger.java 1.1 Mon, 02 May 2005 14:31:03 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999 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: import java.math.BigInteger;
024:
025: /** Infinite precision integers with an plus and minus infinity.
026: *
027: * <p>This type is intended to support reasoning like that done by
028: * Eric Hehner for the time behavior of programs. Of course, it could
029: * also be used for other purposes as well.
030: *
031: * @version $Revision: 1.1 $
032: * @author Gary T. Leavens
033: * @see java.math.BigInteger
034: */
035: //-@ immutable
036: public/*@ pure @*/interface JMLInfiniteInteger extends JMLComparable {
037: /** Does this object represent a nonnegative integer? */
038: //@ public model instance boolean nonnegative;
039: /** The sign of this integer. */
040: //@ public model instance int sign; in nonnegative;
041: //@ public invariant sign == -1 || sign == 0 || sign == +1;
042: //@ public instance represents nonnegative <- sign >= 0;
043: /** Is this integer infinite? */
044: //@ public model instance boolean is_infinite;
045: /** If this integer is not infinite, its finite value. */
046: //@ public model instance BigInteger finite_value;
047: /*@ public instance invariant sign == -1 || sign == 0 || sign == +1;
048: @ public instance invariant
049: @ !is_infinite ==> finite_value != null
050: @ && sign == finite_value.signum();
051: @*/
052: /*@ public instance invariant_redundantly
053: @ sign == 0 <==> !is_infinite
054: @ && finite_value.equals(BigInteger.ZERO);
055: @*/
056:
057: //@ public instance constraint nonnegative == \old(nonnegative);
058: //@ public instance constraint sign == \old(sign);
059: //@ public instance constraint is_infinite == \old(is_infinite);
060: //@ public instance constraint finite_value == \old(finite_value);
061: /** Return the sign of this integer.
062: */
063: /*@ public normal_behavior
064: @ ensures \result == sign;
065: @ implies_that
066: @ public normal_behavior
067: @ ensures \result == -1 || \result == 0 || \result == +1;
068: @ ensures (\result == 0 || \result == +1) <==> nonnegative;
069: @ ensures \result == -1 <==> !nonnegative;
070: @*/
071: int signum();
072:
073: /** Tell if this integer is finite.
074: */
075: /*@ public normal_behavior
076: @ ensures \result == !is_infinite;
077: @*/
078: boolean isFinite();
079:
080: /** Assuming this integer is finite, return its value.
081: */
082: /*@ public normal_behavior
083: @ requires !is_infinite;
084: @ ensures \result != null && \result.equals(finite_value);
085: @ also
086: @ public exceptional_behavior
087: @ requires is_infinite;
088: @ signals (ArithmeticException);
089: @*/
090: /*@ non_null @*/BigInteger finiteValue()
091: throws ArithmeticException;
092:
093: /** Compare this to o, returning a comparison code.
094: * @param o the object this is compared to.
095: * @exception ClassCastException when o is not
096: * a JMLInfiniteInteger or a BigInteger.
097: * @see #equals(Object)
098: * @see #greaterThanOrEqualTo
099: * @see #greaterThan
100: * @see #lessThanOrEqualTo
101: * @see #lessThan
102: */
103: /*@ also
104: @ public normal_behavior
105: @ requires o != null && o instanceof JMLInfiniteInteger;
106: @ {|
107: @ old JMLInfiniteInteger n = (JMLInfiniteInteger)o;
108: @ {|
109: @ requires lessThan(n);
110: @ ensures \result == -1;
111: @ also
112: @ requires equals(n);
113: @ ensures \result == 0;
114: @ also
115: @ requires greaterThan(n);
116: @ ensures \result == +1;
117: @ |}
118: @ |}
119: @ also
120: @ public normal_behavior
121: @ requires o != null && o instanceof BigInteger;
122: @ {|
123: @ requires is_infinite && !nonnegative;
124: @ ensures \result == -1;
125: @ also
126: @ requires !is_infinite;
127: @ ensures \result == finite_value.compareTo((BigInteger)o);
128: @ also
129: @ requires is_infinite && nonnegative;
130: @ ensures \result == +1;
131: @ |}
132: @ also
133: @ public exceptional_behavior
134: @ requires o != null
135: @ && !(o instanceof JMLInfiniteInteger)
136: @ && !(o instanceof BigInteger);
137: @ signals (ClassCastException);
138: @*/
139: int compareTo(Object o) throws ClassCastException;
140:
141: /** Tell whether this integer is equal to the argument.
142: ** Note that comparisons to BigIntegers are also handled.
143: * @see #compareTo(Object)
144: * @see #greaterThanOrEqualTo
145: * @see #greaterThan
146: * @see #lessThanOrEqualTo
147: * @see #lessThan
148: */
149: /*@ also
150: @ public normal_behavior
151: @ requires o != null && o instanceof JMLInfiniteInteger;
152: @ {|
153: @ old JMLInfiniteInteger n = (JMLInfiniteInteger)o;
154: @ ensures \result <==>
155: @ sign == n.sign
156: @ && is_infinite == n.is_infinite
157: @ && (!is_infinite && !n.is_infinite
158: @ ==> finite_value.compareTo(n.finite_value) == 0);
159: @ |}
160: @ also
161: @ public normal_behavior
162: @ requires o != null && o instanceof BigInteger;
163: @ {|
164: @ old BigInteger bi = (BigInteger)o;
165: @ ensures \result <==>
166: @ !is_infinite && finite_value.compareTo(bi) == 0;
167: @ |}
168: @ also
169: @ public normal_behavior
170: @ requires o == null
171: @ || !(o instanceof BigInteger || o instanceof JMLInfiniteInteger);
172: @ ensures !\result;
173: @*/
174: boolean equals(Object o);
175:
176: /** Tell if this integer is greater than or equal to the argument.
177: * @see #equals(Object)
178: * @see #compareTo(Object)
179: * @see #greaterThan
180: * @see #lessThanOrEqualTo
181: * @see #lessThan
182: */
183: /*@ public normal_behavior
184: @ requires n != null;
185: @ ensures \result <==>
186: @ (is_infinite ==>
187: @ (nonnegative || (!n.nonnegative && n.is_infinite)))
188: @ && (!is_infinite
189: @ ==> finite_value.compareTo(n.finite_value) >= 0);
190: @ implies_that
191: @ public normal_behavior
192: @ requires n != null;
193: @ {|
194: @ requires (nonnegative && is_infinite)
195: @ || (!n.nonnegative && n.is_infinite);
196: @ ensures \result;
197: @ also
198: @ requires (n.nonnegative && n.is_infinite)
199: @ || (!nonnegative && is_infinite);
200: @ ensures !\result;
201: @ also
202: @ requires !is_infinite && !n.is_infinite;
203: @ ensures \result <==>
204: @ finite_value.compareTo(n.finite_value) >= 0;
205: @ |}
206: @*/
207: boolean greaterThanOrEqualTo(/*@ non_null @*/JMLInfiniteInteger n);
208:
209: /** Tell if this integer is less than or equal to the argument.
210: * @see #equals(Object)
211: * @see #compareTo(Object)
212: * @see #greaterThanOrEqualTo
213: * @see #greaterThan
214: * @see #lessThan
215: */
216: /*@ public normal_behavior
217: @ requires n != null;
218: @ ensures \result <==> n.greaterThanOrEqualTo(this);
219: @*/
220: boolean lessThanOrEqualTo(/*@ non_null @*/JMLInfiniteInteger n);
221:
222: /** Tell if this integer is strictly greater than the argument.
223: * @see #equals(Object)
224: * @see #compareTo(Object)
225: * @see #greaterThanOrEqualTo
226: * @see #lessThanOrEqualTo
227: * @see #lessThan
228: */
229: /*@ public normal_behavior
230: @ requires n != null;
231: @ ensures \result <==> !equals(n) && greaterThanOrEqualTo(n);
232: @*/
233: boolean greaterThan(/*@ non_null @*/JMLInfiniteInteger n);
234:
235: /** Tell if this integer is strictly less than the argument.
236: * @see #equals(Object)
237: * @see #compareTo(Object)
238: * @see #greaterThanOrEqualTo
239: * @see #greaterThan
240: * @see #lessThanOrEqualTo
241: */
242: /*@ public normal_behavior
243: @ requires n != null;
244: @ ensures \result <==> !equals(n) && lessThanOrEqualTo(n);
245: @*/
246: boolean lessThan(/*@ non_null @*/JMLInfiniteInteger n);
247:
248: /** Return a hash code for this integer.
249: */
250: int hashCode();
251:
252: /** Return the absolute value of this integer.
253: * @see #negate
254: */
255: /*@ public normal_behavior
256: @ ensures \result != null && \result.nonnegative
257: @ && \result.is_infinite == is_infinite
258: @ && (!\result.is_infinite
259: @ ==> \result.finite_value.equals(finite_value.abs()));
260: @*/
261: /*@ non_null @*/JMLInfiniteInteger abs();
262:
263: /** Return the maximum of this integer and the argument.
264: * @see #min
265: */
266: /*@ public normal_behavior
267: @ requires n != null;
268: @ {|
269: @ requires this.greaterThanOrEqualTo(n);
270: @ ensures \result.equals(this);
271: @ also
272: @ requires n.greaterThanOrEqualTo(this);
273: @ ensures \result.equals(n);
274: @ |}
275: @*/
276: /*@ non_null @*/JMLInfiniteInteger max(
277: /*@ non_null @*/JMLInfiniteInteger n);
278:
279: /** Return the minimum of this integer and the argument.
280: * @see #max
281: */
282: /*@ public normal_behavior
283: @ requires n != null;
284: @ {|
285: @ requires this.lessThanOrEqualTo(n);
286: @ ensures \result.equals(this);
287: @ also
288: @ requires n.lessThanOrEqualTo(this);
289: @ ensures \result.equals(n);
290: @ |}
291: @*/
292: /*@ non_null @*/JMLInfiniteInteger min(
293: /*@ non_null @*/JMLInfiniteInteger n);
294:
295: /** Return the negation of this integer.
296: * @see #abs
297: * @see #subtract
298: */
299: /*@ public normal_behavior
300: @ ensures \result != null && \result.sign == -1 * sign;
301: @ also
302: @ requires is_infinite;
303: @ ensures \result.is_infinite;
304: @ also
305: @ requires !is_infinite;
306: @ ensures !\result.is_infinite
307: @ && \result.finite_value.equals(finite_value.negate());
308: @*/
309: /*@ non_null @*/JMLInfiniteInteger negate();
310:
311: /** Return the sum of this integer and the argument.
312: * @see #subtract
313: */
314: /*@ public normal_behavior
315: @ requires n != null;
316: @ {|
317: @ ensures \result != null;
318: @ also
319: @ requires is_infinite && !n.is_infinite;
320: @ ensures \result.equals(this);
321: @ also
322: @ requires !is_infinite && n.is_infinite;
323: @ ensures \result.equals(n);
324: @ also
325: @ requires is_infinite && n.is_infinite;
326: @ {|
327: @ requires nonnegative == n.nonnegative;
328: @ ensures \result.equals(this);
329: @ also
330: @ requires nonnegative != n.nonnegative;
331: @ ensures \result.equals(new BigInteger("0"));
332: @ |}
333: @ also
334: @ requires !is_infinite && !n.is_infinite;
335: @ ensures !\result.is_infinite
336: @ && \result.finite_value.equals(finite_value.add(n.finite_value));
337: @ |}
338: @*/
339: /*@ non_null @*/JMLInfiniteInteger add(
340: /*@ non_null @*/JMLInfiniteInteger n);
341:
342: /** Return the difference between this integer and the argument.
343: * @see #add
344: * @see #negate
345: */
346: /*@ public normal_behavior
347: @ requires n != null;
348: @ {|
349: @ ensures \result != null;
350: @ also
351: @ requires is_infinite && !n.is_infinite;
352: @ ensures \result.equals(this);
353: @ also
354: @ requires !is_infinite && n.is_infinite;
355: @ ensures \result.equals(n.negate());
356: @ also
357: @ requires is_infinite && n.is_infinite;
358: @ {|
359: @ requires nonnegative == n.nonnegative;
360: @ ensures \result.equals(new BigInteger("0"));
361: @ also
362: @ requires nonnegative != n.nonnegative;
363: @ ensures \result.equals(this);
364: @ |}
365: @ also
366: @ requires !is_infinite && !n.is_infinite;
367: @ ensures !\result.is_infinite
368: @ && \result.finite_value.equals(finite_value.subtract(n.finite_value));
369: @ |}
370: @*/
371: /*@ non_null @*/JMLInfiniteInteger subtract(
372: /*@ non_null @*/JMLInfiniteInteger n);
373:
374: /** Return the product of this integer and the argument.
375: * @see #divide
376: * @see #remainder
377: * @see #mod
378: */
379: /*@ public normal_behavior
380: @ requires n != null;
381: @ {|
382: @ ensures \result != null && \result.sign == sign * n.sign;
383: @ also
384: @ requires equals(new BigInteger("0"))
385: @ || n.equals(new BigInteger("0"));
386: @ ensures \result.equals(new BigInteger("0"));
387: @ also
388: @ requires !(equals(new BigInteger("0"))
389: @ || n.equals(new BigInteger("0")));
390: @ {|
391: @ requires is_infinite || n.is_infinite;
392: @ ensures \result.is_infinite;
393: @ also
394: @ requires !is_infinite && !n.is_infinite;
395: @ ensures !\result.is_infinite
396: @ && \result.finite_value.equals(finite_value.multiply(n.finite_value));
397: @ |}
398: @ |}
399: @*/
400: /*@ non_null @*/JMLInfiniteInteger multiply(
401: /*@ non_null @*/JMLInfiniteInteger n);
402:
403: /** Return the quotient of this integer divided by the argument.
404: * @see #multiply
405: * @see #remainder
406: * @see #mod
407: */
408: /*@ public normal_behavior
409: @ requires n != null && n.sign != 0;
410: @ {|
411: @ ensures \result != null
412: @ && (\result.sign == 0|| \result.sign == sign * n.sign);
413: @ also
414: @ requires is_infinite && n.is_infinite;
415: @ ensures !\result.is_infinite
416: @ && \result.abs().equals(new BigInteger("1"));
417: @ also
418: @ requires is_infinite && !n.is_infinite;
419: @ ensures \result.is_infinite;
420: @ also
421: @ requires !is_infinite && n.is_infinite;
422: @ ensures \result.equals(new BigInteger("0"));
423: @ also
424: @ requires !is_infinite && !n.is_infinite;
425: @ ensures !\result.is_infinite
426: @ && \result.finite_value.equals(finite_value.divide(n.finite_value));
427: @ |}
428: @ also
429: @ public exceptional_behavior
430: @ requires n != null && n.sign == 0;
431: @ signals (ArithmeticException);
432: @*/
433: /*@ non_null @*/JMLInfiniteInteger divide(
434: /*@ non_null @*/JMLInfiniteInteger n)
435: throws ArithmeticException;
436:
437: /** Return the remainder of this integer divided by the argument.
438: * @see #divide
439: * @see #mod
440: */
441: /*@ public normal_behavior
442: @ requires n != null && n.sign != 0;
443: @ {|
444: @ ensures \result != null;
445: @ also
446: @ requires is_infinite;
447: @ ensures \result.equals(new BigInteger("0"));
448: @ also
449: @ requires !is_infinite && n.is_infinite;
450: @ ensures \result.abs().equals(this.abs());
451: @ ensures \result.sign == sign * n.sign;
452: @ also
453: @ requires !is_infinite && !n.is_infinite;
454: @ ensures !\result.is_infinite
455: @ && \result.finite_value
456: @ .equals(finite_value.remainder(n.finite_value));
457: @ |}
458: @ also
459: @ public exceptional_behavior
460: @ requires n != null && n.sign == 0;
461: @ signals (ArithmeticException);
462: @*/
463: /*@ non_null @*/JMLInfiniteInteger remainder(
464: /*@ non_null @*/JMLInfiniteInteger n)
465: throws ArithmeticException;
466:
467: /** Return this integer modulo the argument.
468: * @see #divide
469: * @see #remainder
470: */
471: /*@ public normal_behavior
472: @ requires n != null && n.sign == +1;
473: @ {|
474: @ ensures \result != null && \result.sign >= 0;
475: @ also
476: @ requires is_infinite;
477: @ ensures \result.equals(new BigInteger("0"));
478: @ also
479: @ requires !is_infinite && n.is_infinite;
480: @ ensures \result.equals(n);
481: @ also
482: @ requires !is_infinite && !n.is_infinite;
483: @ ensures !\result.is_infinite
484: @ && \result.finite_value.equals(finite_value.mod(n.finite_value));
485: @ |}
486: @ also
487: @ public exceptional_behavior
488: @ requires n != null && n.sign != +1;
489: @ signals (ArithmeticException);
490: @*/
491: /*@ non_null @*/JMLInfiniteInteger mod(
492: /*@ non_null @*/JMLInfiniteInteger n)
493: throws ArithmeticException;
494:
495: /** Return this integer raised to the argument's power.
496: */
497: /*@ public normal_behavior
498: @ requires n >= 0;
499: @ {|
500: @ ensures \result != null
501: @ && (\result.nonnegative <==> n % 2 == 0 || nonnegative);
502: @ also
503: @ requires is_infinite;
504: @ ensures n != 0 ==> \result.is_infinite;
505: @ ensures n == 0
506: @ ==> !\result.is_infinite
507: @ && \result.finite_value.equals(new BigInteger("1"));
508: @ also
509: @ requires !is_infinite;
510: @ ensures !\result.is_infinite
511: @ && \result.finite_value.equals(finite_value.pow(n));
512: @ |}
513: @ also
514: @ public exceptional_behavior
515: @ requires n < 0;
516: @ signals (ArithmeticException);
517: @*/
518: /*@ non_null @*/JMLInfiniteInteger pow(int n)
519: throws ArithmeticException;
520:
521: /** Return this integer approximated by a double.
522: * @see #floatValue
523: */
524: /*@ public normal_behavior
525: @ requires is_infinite && nonnegative;
526: @ ensures \result == Double.POSITIVE_INFINITY;
527: @ also
528: @ requires is_infinite && !nonnegative;
529: @ ensures \result == Double.NEGATIVE_INFINITY;
530: @ also
531: @ requires !is_infinite;
532: @ ensures \result == finite_value.doubleValue();
533: @*/
534: double doubleValue();
535:
536: /** Return this integer approximated by a float.
537: * @see #doubleValue
538: */
539: /*@ public normal_behavior
540: @ requires is_infinite && nonnegative;
541: @ ensures \result == Float.POSITIVE_INFINITY;
542: @ also
543: @ requires is_infinite && !nonnegative;
544: @ ensures \result == Float.NEGATIVE_INFINITY;
545: @ also
546: @ requires !is_infinite;
547: @ ensures \result == finite_value.floatValue();
548: @*/
549: float floatValue();
550:
551: /** Return the decimal representation of this integer.
552: * @see #toString(int)
553: */
554: /*@ also
555: @ public normal_behavior
556: @ ensures \result.equals(toString(10));
557: @*/
558: String toString();
559:
560: /** Return the digits representing this integer in the given radix.
561: * @see #toString()
562: */
563: String toString(int radix)
564: /*@ public model_program {
565: @ if (is_infinite) {
566: @ if (nonnegative) {
567: @ return "Infinity";
568: @ } else {
569: @ return "-Infinity";
570: @ }
571: @ } else {
572: @ return finite_value.toString(radix);
573: @ }
574: @ }
575: @*/
576: ;
577: }
|