JML

org.jmlspecs.models.resolve
Class NaturalNumber

java.lang.Object
  extended byjava.lang.Number
      extended byorg.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.25 $
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.

Constructor Detail

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)
Method Detail

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

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.