org.jmlspecs.models.resolve
Class NaturalNumber

java.lang.Object
  java.lang.Number
      org.jmlspecs.models.resolve.NaturalNumber

All Implemented Interfaces:

AntisymmetricCompareTo, Cloneable, Comparable, CompareTo, JMLType, PreorderedCompareTo, ReflexiveCompareTo, Serializable, TotalCompareTo, TotallyOrderedCompareTo, TotalPreorderedCompareTo, TransitiveCompareTo

public class NaturalNumber

extends Number

implements TotallyOrderedCompareTo, JMLType

The natural numbers. These are essentially unlimited in size.

Version:

$Revision: 1.22 $

Author:

Gary T. Leavens

See Also:

BigInteger, JMLFiniteInteger

Field Summary
private static NaturalNumber	intMaxVal           The maximum integer as a natural number.
static NaturalNumber	ONE           The natural number one.
private  BigInteger	value           The value of this natural number.
static NaturalNumber	ZERO           The natural number zero.

 

Fields inherited from class java.lang.Number

 

Constructor Summary

NaturalNumber()           Initialize this natural number to zero.

NaturalNumber(BigInteger val)           Initialize this natural number to the given BigInteger value.

NaturalNumber(long val)           Initialize this natural number to the given long value.

 

Method Summary
NaturalNumber	add(NaturalNumber val)           Return the sum of this natural number and the given one.
BigInteger	bigIntegerValue()           Return the BigInteger value of this natural number.
Object	clone()           Return a clone of this object.
int	compareTo(Object o)           Compare this to obj, returning negative if this is strictly less than obj, 0 if they are equal, and positive otherwise.
int	compareTo(NaturalNumber val)           Return negative if this natural numbers strictly less than the given one, 0 if they are equal, and positive if this natural numbers is strictly greater than the given one.
NaturalNumber	divide(NaturalNumber val)           Return the quotient of this natural number divided by the given one.
boolean	divides(NaturalNumber val)           Tell if this natural number divides the given one evenly.
double	doubleValue()
boolean	equals(Object x)           Tell if this object is equal to the given argument.
float	floatValue()
NaturalNumber	gcd(NaturalNumber val)           Return the greatest common denominator of this number and the given number.
int	hashCode()           Return a hash code for this object.
int	intValue()
boolean	isZero()           Tell if this object is equal to zero.
long	longValue()
NaturalNumber	max(NaturalNumber val)           Return the smaller of the given natural number and this one.
NaturalNumber	min(NaturalNumber val)           Return the smaller of the given natural number and this one.
NaturalNumber	mod(NaturalNumber m)           Return this natural number modulo the given one.
NaturalNumber	multiply(NaturalNumber val)           Return the product of this natural number and the given one.
NaturalNumber	pow(int exponent)           Return this natural number multiplied by itself the given number of times.
NaturalNumber	pow(NaturalNumber exponent)           Return this natural number multiplied by itself the given number of times.
NaturalNumber	remainder(NaturalNumber val)           Return the remainder of this natural number divided by the given one.
NaturalNumber	shiftLeft(int n)           Return this natural number left shifted the given number of bits.
NaturalNumber	shiftRight(int n)           Return this natural number right shifted the given number of bits.
NaturalNumber	suc()           Return the successor of this natural number.
static NaturalNumber	suc(NaturalNumber v)           Return the successor of the given natural number.
String	toString()
static NaturalNumber	valueOf(long val)           Return a natural number with the given value.

 

Methods inherited from class java.lang.Number

byteValue, shortValue

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

value

private final BigInteger value

The value of this natural number.

ZERO

public static final NaturalNumber ZERO

The natural number zero.

See Also:

NaturalNumber(), ONE

ONE

public static final NaturalNumber ONE

The natural number one.

See Also:

NaturalNumber(long), valueOf(long), ZERO

intMaxVal

private static final NaturalNumber intMaxVal

The maximum integer as a natural number.

NaturalNumber

public NaturalNumber()

Initialize this natural number to zero.

See Also:

ZERO, NaturalNumber(long), NaturalNumber(BigInteger)

NaturalNumber

public NaturalNumber(long val)
              throws IllegalArgumentException

Initialize this natural number to the given long value.

Throws:

IllegalArgumentException

See Also:

NaturalNumber(), NaturalNumber(BigInteger), valueOf(long)

NaturalNumber

public NaturalNumber(BigInteger val)
              throws IllegalArgumentException

Initialize this natural number to the given BigInteger value.

Throws:

IllegalArgumentException

See Also:

NaturalNumber(), NaturalNumber(BigInteger)

valueOf

public static NaturalNumber valueOf(long val)

Return a natural number with the given value.

See Also:

NaturalNumber(long), NaturalNumber(BigInteger)

suc

public NaturalNumber suc()

Return the successor of this natural number.

See Also:

suc(NaturalNumber), add(org.jmlspecs.models.resolve.NaturalNumber), ONE

suc

public static NaturalNumber suc(NaturalNumber v)

Return the successor of the given natural number.

See Also:

suc(), add(org.jmlspecs.models.resolve.NaturalNumber)

add

public NaturalNumber add(NaturalNumber val)

Return the sum of this natural number and the given one.

See Also:

suc(), add(org.jmlspecs.models.resolve.NaturalNumber)

multiply

public NaturalNumber multiply(NaturalNumber val)

Return the product of this natural number and the given one.

See Also:

divide(org.jmlspecs.models.resolve.NaturalNumber)

divide

public NaturalNumber divide(NaturalNumber val)

Return the quotient of this natural number divided by the given one.

See Also:

multiply(org.jmlspecs.models.resolve.NaturalNumber)

remainder

public NaturalNumber remainder(NaturalNumber val)

Return the remainder of this natural number divided by the given one.

See Also:

divide(org.jmlspecs.models.resolve.NaturalNumber)

pow

public NaturalNumber pow(NaturalNumber exponent)
                  throws OutOfMemoryError

Return this natural number multiplied by itself the given number of times.

Throws:

OutOfMemoryError

See Also:

multiply(org.jmlspecs.models.resolve.NaturalNumber), pow(int)

pow

public NaturalNumber pow(int exponent)

Return this natural number multiplied by itself the given number of times.

See Also:

multiply(org.jmlspecs.models.resolve.NaturalNumber), pow(NaturalNumber)

gcd

public NaturalNumber gcd(NaturalNumber val)

Return the greatest common denominator of this number and the given number.

mod

public NaturalNumber mod(NaturalNumber m)

Return this natural number modulo the given one.

See Also:

remainder(org.jmlspecs.models.resolve.NaturalNumber)

shiftLeft

public NaturalNumber shiftLeft(int n)

Return this natural number left shifted the given number of bits.

See Also:

shiftRight(int), pow(int)

shiftRight

public NaturalNumber shiftRight(int n)

Return this natural number right shifted the given number of bits.

See Also:

shiftLeft(int), pow(int)

compareTo

public int compareTo(NaturalNumber val)

Return negative if this natural numbers strictly less than the given one, 0 if they are equal, and positive if this natural numbers is strictly greater than the given one.

See Also:

compareTo(Object), equals(java.lang.Object)

compareTo

public int compareTo(Object o)
              throws ClassCastException

Description copied from interface: CompareTo

Compare this to obj, returning negative if this is strictly less than obj, 0 if they are equal, and positive otherwise.

Specified by:

compareTo in interface CompareTo

Throws:

ClassCastException

equals

public boolean equals(Object x)

Tell if this object is equal to the given argument.

Specified by:

equals in interface JMLType

Overrides:

equals in class Object

See Also:

compareTo(Object), compareTo(NaturalNumber), equals(java.lang.Object)

clone

public Object clone()

Description copied from interface: JMLType

Return a clone of this object.

Specified by:

clone in interface JMLType

Overrides:

clone in class Object

isZero

public boolean isZero()

Tell if this object is equal to zero.

See Also:

ZERO, compareTo(NaturalNumber), equals(java.lang.Object)

divides

public boolean divides(NaturalNumber val)

Tell if this natural number divides the given one evenly.

See Also:

remainder(org.jmlspecs.models.resolve.NaturalNumber), mod(org.jmlspecs.models.resolve.NaturalNumber)

min

public NaturalNumber min(NaturalNumber val)

Return the smaller of the given natural number and this one.

See Also:

max(org.jmlspecs.models.resolve.NaturalNumber), compareTo(NaturalNumber)

max

public NaturalNumber max(NaturalNumber val)

Return the smaller of the given natural number and this one.

See Also:

max(org.jmlspecs.models.resolve.NaturalNumber), compareTo(NaturalNumber)

hashCode

public int hashCode()

Description copied from interface: JMLType

Return a hash code for this object.

Specified by:

hashCode in interface JMLType

Overrides:

hashCode in class Object

toString

public String toString()

Overrides:

toString in class Object

bigIntegerValue

public BigInteger bigIntegerValue()

Return the BigInteger value of this natural number.

See Also:

intValue(), longValue()

intValue

public int intValue()

longValue

public long longValue()

floatValue

public float floatValue()

doubleValue

public double doubleValue()