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()