JML

org.jmlspecs.models
Interface JMLInfiniteInteger

All Superinterfaces:
Cloneable, Comparable, JMLComparable, JMLType, Serializable
All Known Implementing Classes:
JMLInfiniteIntegerClass

public interface JMLInfiniteInteger
extends JMLComparable

Infinite precision integers with an plus and minus infinity.

This type is intended to support reasoning like that done by Eric Hehner for the time behavior of programs. Of course, it could also be used for other purposes as well.

Version:
$Revision: 1.34 $
Author:
Gary T. Leavens
See Also:
BigInteger

Method Summary
 JMLInfiniteInteger abs()
          Return the absolute value of this integer.
 JMLInfiniteInteger add(JMLInfiniteInteger n)
          Return the sum of this integer and the argument.
 int compareTo(Object o)
          Compare this to o, returning a comparison code.
 JMLInfiniteInteger divide(JMLInfiniteInteger n)
          Return the quotient of this integer divided by the argument.
 double doubleValue()
          Return this integer approximated by a double.
 boolean equals(Object o)
          Tell whether this integer is equal to the argument.
 BigInteger finiteValue()
          Assuming this integer is finite, return its value.
 float floatValue()
          Return this integer approximated by a float.
 boolean greaterThan(JMLInfiniteInteger n)
          Tell if this integer is strictly greater than the argument.
 boolean greaterThanOrEqualTo(JMLInfiniteInteger n)
          Tell if this integer is greater than or equal to the argument.
 int hashCode()
          Return a hash code for this integer.
 boolean isFinite()
          Tell if this integer is finite.
 boolean lessThan(JMLInfiniteInteger n)
          Tell if this integer is strictly less than the argument.
 boolean lessThanOrEqualTo(JMLInfiniteInteger n)
          Tell if this integer is less than or equal to the argument.
 JMLInfiniteInteger max(JMLInfiniteInteger n)
          Return the maximum of this integer and the argument.
 JMLInfiniteInteger min(JMLInfiniteInteger n)
          Return the minimum of this integer and the argument.
 JMLInfiniteInteger mod(JMLInfiniteInteger n)
          Return this integer modulo the argument.
 JMLInfiniteInteger multiply(JMLInfiniteInteger n)
          Return the product of this integer and the argument.
 JMLInfiniteInteger negate()
          Return the negation of this integer.
 JMLInfiniteInteger pow(int n)
          Return this integer raised to the argument's power.
 JMLInfiniteInteger remainder(JMLInfiniteInteger n)
          Return the remainder of this integer divided by the argument.
 int signum()
          Does this object represent a nonnegative integer?
 JMLInfiniteInteger subtract(JMLInfiniteInteger n)
          Return the difference between this integer and the argument.
 String toString()
          Return the decimal representation of this integer.
 String toString(int radix)
          Return the digits representing this integer in the given radix.
 
Methods inherited from interface org.jmlspecs.models.JMLType
clone
 

Method Detail

signum

public int signum()
Does this object represent a nonnegative integer? The sign of this integer. Is this integer infinite? If this integer is not infinite, its finite value. Return the sign of this integer.


isFinite

public boolean isFinite()
Tell if this integer is finite.


finiteValue

public BigInteger finiteValue()
                                throws ArithmeticException
Assuming this integer is finite, return its value.

Throws:
ArithmeticException

compareTo

public int compareTo(Object o)
                       throws ClassCastException
Compare this to o, returning a comparison code.

Specified by:
compareTo in interface JMLComparable
Parameters:
o - the object this is compared to.
Throws:
ClassCastException - when o is not a JMLInfiniteInteger or a BigInteger.
See Also:
equals(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)

equals

public boolean equals(Object o)
Tell whether this integer is equal to the argument. Note that comparisons to BigIntegers are also handled.

Specified by:
equals in interface JMLType
See Also:
compareTo(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)

greaterThanOrEqualTo

public boolean greaterThanOrEqualTo(JMLInfiniteInteger n)
Tell if this integer is greater than or equal to the argument.

See Also:
equals(Object), compareTo(Object), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)

lessThanOrEqualTo

public boolean lessThanOrEqualTo(JMLInfiniteInteger n)
Tell if this integer is less than or equal to the argument.

See Also:
equals(Object), compareTo(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)

greaterThan

public boolean greaterThan(JMLInfiniteInteger n)
Tell if this integer is strictly greater than the argument.

See Also:
equals(Object), compareTo(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)

lessThan

public boolean lessThan(JMLInfiniteInteger n)
Tell if this integer is strictly less than the argument.

See Also:
equals(Object), compareTo(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger)

hashCode

public int hashCode()
Return a hash code for this integer.

Specified by:
hashCode in interface JMLType

abs

public JMLInfiniteInteger abs()
Return the absolute value of this integer.

See Also:
negate()

max

public JMLInfiniteInteger max(JMLInfiniteInteger n)
Return the maximum of this integer and the argument.

See Also:
min(org.jmlspecs.models.JMLInfiniteInteger)

min

public JMLInfiniteInteger min(JMLInfiniteInteger n)
Return the minimum of this integer and the argument.

See Also:
max(org.jmlspecs.models.JMLInfiniteInteger)

negate

public JMLInfiniteInteger negate()
Return the negation of this integer.

See Also:
abs(), subtract(org.jmlspecs.models.JMLInfiniteInteger)

add

public JMLInfiniteInteger add(JMLInfiniteInteger n)
Return the sum of this integer and the argument.

See Also:
subtract(org.jmlspecs.models.JMLInfiniteInteger)

subtract

public JMLInfiniteInteger subtract(JMLInfiniteInteger n)
Return the difference between this integer and the argument.

See Also:
add(org.jmlspecs.models.JMLInfiniteInteger), negate()

multiply

public JMLInfiniteInteger multiply(JMLInfiniteInteger n)
Return the product of this integer and the argument.

See Also:
divide(org.jmlspecs.models.JMLInfiniteInteger), remainder(org.jmlspecs.models.JMLInfiniteInteger), mod(org.jmlspecs.models.JMLInfiniteInteger)

divide

public JMLInfiniteInteger divide(JMLInfiniteInteger n)
                                   throws ArithmeticException
Return the quotient of this integer divided by the argument.

Throws:
ArithmeticException
See Also:
multiply(org.jmlspecs.models.JMLInfiniteInteger), remainder(org.jmlspecs.models.JMLInfiniteInteger), mod(org.jmlspecs.models.JMLInfiniteInteger)

remainder

public JMLInfiniteInteger remainder(JMLInfiniteInteger n)
                                      throws ArithmeticException
Return the remainder of this integer divided by the argument.

Throws:
ArithmeticException
See Also:
divide(org.jmlspecs.models.JMLInfiniteInteger), mod(org.jmlspecs.models.JMLInfiniteInteger)

mod

public JMLInfiniteInteger mod(JMLInfiniteInteger n)
                                throws ArithmeticException
Return this integer modulo the argument.

Throws:
ArithmeticException
See Also:
divide(org.jmlspecs.models.JMLInfiniteInteger), remainder(org.jmlspecs.models.JMLInfiniteInteger)

pow

public JMLInfiniteInteger pow(int n)
                                throws ArithmeticException
Return this integer raised to the argument's power.

Throws:
ArithmeticException

doubleValue

public double doubleValue()
Return this integer approximated by a double.

See Also:
floatValue()

floatValue

public float floatValue()
Return this integer approximated by a float.

See Also:
doubleValue()

toString

public String toString()
Return the decimal representation of this integer.

See Also:
toString(int)

toString

public String toString(int radix)
Return the digits representing this integer in the given radix.

See Also:
toString()

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.