org.jmlspecs.models
Class JMLFiniteInteger

java.lang.Object
  org.jmlspecs.models.JMLInfiniteIntegerClass
      org.jmlspecs.models.JMLFiniteInteger

All Implemented Interfaces:

Cloneable, Comparable, JMLComparable, JMLInfiniteInteger, JMLType, Serializable

public class JMLFiniteInteger

extends JMLInfiniteIntegerClass

Arbitrary precision integers with a finite value.

Version:

$Revision: 1.23 $

Author:

Gary T. Leavens

See Also:

BigInteger

Class Specifications

public invariant !this.is_infinite; protected represents finite_value <- this.val; protected represents sign <- this.val.signum(); protected represents is_infinite <- false;

Specifications inherited from class JMLInfiniteIntegerClass

public invariant this.owner == null;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface JMLInfiniteInteger

public invariant this.sign == -1||this.sign == 0||this.sign == 1; instance public invariant this.sign == -1||this.sign == 0||this.sign == 1; instance public invariant !this.is_infinite ==> this.finite_value != null&&this.sign == this.finite_value.signum(); instance public invariant_redundantly this.sign == 0 <==> !this.is_infinite&&this.finite_value.equals(java.math.BigInteger.ZERO); instance public constraint this.nonnegative == \old(this.nonnegative); instance public constraint this.sign == \old(this.sign); instance public constraint this.is_infinite == \old(this.is_infinite); instance public constraint this.finite_value == \old(this.finite_value); instance public represents nonnegative <- this.sign >= 0;

Specifications inherited from interface Comparable

instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0); instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x))); instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n)); instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n)); instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface org.jmlspecs.models.JMLInfiniteInteger

finite_value, is_infinite, nonnegative, sign

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
static JMLFiniteInteger	ONE           The number one (1).
protected  BigInteger	val
static JMLFiniteInteger	ZERO           The number zero (0).

 

Constructor Summary

JMLFiniteInteger()           Initialize this finite integer to zero (0).

JMLFiniteInteger(non_null BigInteger n)           Initialize this finite integer from the given BigInteger.

JMLFiniteInteger(long n)           Initialize this finite integer from the given long.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

 

Method Summary
JMLInfiniteInteger	add(JMLInfiniteInteger n)           Return the sum of this integer and the argument.
int	compareTo(non_null Object o)           Compare this to o, returning a comparison code.
int	compareTo(JMLInfiniteInteger n)           Compare this to the given integer, 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.
BigInteger	finiteValue()           Return the value of this integer.
float	floatValue()           Return this integer approximated by a float.
int	hashCode()           Return a hash code for this object.
int	intValue()           Converts this BigInteger to an integer
boolean	isFinite()           Return true.
long	longValue()           Converts this BigInteger to a long
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()           Return the sign of this 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 class org.jmlspecs.models.JMLInfiniteIntegerClass

abs, clone, equals, greaterThan, greaterThanOrEqualTo, lessThan, lessThanOrEqualTo, max, min

 

Methods inherited from class java.lang.Object

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

 

Field Detail

val

protected final BigInteger val

Specifications: non_null
is in groups: sign finite_value is_infinite

ZERO

public static final JMLFiniteInteger ZERO

The number zero (0).

ONE

public static final JMLFiniteInteger ONE

The number one (1).

JMLFiniteInteger

public JMLFiniteInteger()

Initialize this finite integer to zero (0).

Specifications: (class)pure

public normal_behavior
assignable nonnegative, sign, is_infinite, finite_value;
ensures !this.is_infinite;
ensures this.finite_value.equals(java.math.BigInteger.ZERO);

     also

private normal_behavior
assignable val;

JMLFiniteInteger

public JMLFiniteInteger(non_null BigInteger n)
                 throws IllegalArgumentException

Initialize this finite integer from the given BigInteger.

Throws:

IllegalArgumentException

Specifications: (class)pure

public behavior
assignable nonnegative, sign, is_infinite, finite_value;
ensures !this.is_infinite&&this.finite_value.equals(n);
signals_only java.lang.IllegalArgumentException;
signals (java.lang.IllegalArgumentException) n == null;

JMLFiniteInteger

public JMLFiniteInteger(long n)

Initialize this finite integer from the given long.

Specifications: (class)pure

signum

public int signum()

Return the sign of this integer.

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (class)pure

public normal_behavior
ensures \result == this.sign;

    implies_that

public normal_behavior
ensures \result == -1||\result == 0||\result == 1;
ensures (\result == 0||\result == 1) <==> this.nonnegative;
ensures \result == -1 <==> !this.nonnegative;

isFinite

public boolean isFinite()

Return true.

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (class)pure

public normal_behavior
ensures \result == !this.is_infinite;

finiteValue

public BigInteger finiteValue()

Return the value of this integer.

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
requires !this.is_infinite;
ensures \result != null&&\result .equals(this.finite_value);

     also

public exceptional_behavior
requires this.is_infinite;
signals_only java.lang.ArithmeticException;

compareTo

public int compareTo(JMLInfiniteInteger n)

Compare this to the given integer, returning a comparison code.

Specifications: (class)pure

Specifications inherited from overridden method in class JMLInfiniteIntegerClass:
       (class)pure

Specifications inherited from overridden method compareTo(Object o) in interface JMLInfiniteInteger:
       (class)pure

     also

public normal_behavior
requires o != null&&o instanceof org.jmlspecs.models.JMLInfiniteInteger;

{|

old org.jmlspecs.models.JMLInfiniteInteger n = (org.jmlspecs.models.JMLInfiniteInteger)o;

{|

requires this.lessThan(n);
ensures \result == -1;

also

requires this.equals(n);
ensures \result == 0;

also

requires this.greaterThan(n);
ensures \result == 1;

|}

|}

     also

public normal_behavior
requires o != null&&o instanceof java.math.BigInteger;

{|

requires this.is_infinite&&!this.nonnegative;
ensures \result == -1;

also

requires !this.is_infinite;
ensures \result == this.finite_value.compareTo((java.math.BigInteger)o);

also

requires this.is_infinite&&this.nonnegative;
ensures \result == 1;

|}

     also

public exceptional_behavior
requires o != null&&!(o instanceof org.jmlspecs.models.JMLInfiniteInteger)&&!(o instanceof java.math.BigInteger);
signals_only java.lang.ClassCastException;

Specifications inherited from overridden method compareTo(Object o) in interface JMLComparable:
       (class)pure

     also

public behavior
requires o != null;
ensures (* o is an instance of a comparable class *);
ensures (* if this is equal to o, then \result is 0 *)&&(* if this is less than o, then \result is negative *)&&(* if this is greater than o, then \result is positive *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* o is not an instance of a comparable class *);

Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure

public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);

     also

public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

compareTo

public int compareTo(non_null Object o)
              throws NullPointerException,
                     ClassCastException

Compare this to o, returning a comparison code.

Parameters:

o - the object this is compared to.

Throws:

ClassCastException - when o is not a JMLInfiniteInteger or a BigInteger.

NullPointerException

See Also:

JMLInfiniteInteger.equals(Object), JMLInfiniteInteger.greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.greaterThan(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.lessThan(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method compareTo(Object o) in interface JMLInfiniteInteger:
       (class)pure

     also

public normal_behavior
requires o != null&&o instanceof org.jmlspecs.models.JMLInfiniteInteger;

{|

old org.jmlspecs.models.JMLInfiniteInteger n = (org.jmlspecs.models.JMLInfiniteInteger)o;

{|

requires this.lessThan(n);
ensures \result == -1;

also

requires this.equals(n);
ensures \result == 0;

also

requires this.greaterThan(n);
ensures \result == 1;

|}

|}

     also

public normal_behavior
requires o != null&&o instanceof java.math.BigInteger;

{|

requires this.is_infinite&&!this.nonnegative;
ensures \result == -1;

also

requires !this.is_infinite;
ensures \result == this.finite_value.compareTo((java.math.BigInteger)o);

also

requires this.is_infinite&&this.nonnegative;
ensures \result == 1;

|}

     also

public exceptional_behavior
requires o != null&&!(o instanceof org.jmlspecs.models.JMLInfiniteInteger)&&!(o instanceof java.math.BigInteger);
signals_only java.lang.ClassCastException;

Specifications inherited from overridden method compareTo(Object o) in interface JMLComparable:
       (class)pure

     also

public behavior
requires o != null;
ensures (* o is an instance of a comparable class *);
ensures (* if this is equal to o, then \result is 0 *)&&(* if this is less than o, then \result is negative *)&&(* if this is greater than o, then \result is positive *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* o is not an instance of a comparable class *);

Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure

public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);

     also

public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

hashCode

public int hashCode()

Return a hash code for this object.

Specified by:

hashCode in interface JMLInfiniteInteger

Overrides:

hashCode in class Object

Specifications: (class)pure

Specifications inherited from overridden method in class Object:

public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);

     also

public code normal_behavior
assignable \nothing;

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (class)pure

Specifications inherited from overridden method in interface JMLType:
       pure

negate

public JMLInfiniteInteger negate()

Return the negation of this integer.

See Also:

JMLInfiniteInteger.abs(), JMLInfiniteInteger.subtract(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
ensures \result != null&&\result .sign == -1*this.sign;

     also

requires this.is_infinite;
ensures \result .is_infinite;

     also

requires !this.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.negate());

add

public JMLInfiniteInteger add(JMLInfiniteInteger n)

Return the sum of this integer and the argument.

See Also:

JMLInfiniteInteger.subtract(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method add(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
requires n != null;

{|

ensures \result != null;

also

requires this.is_infinite&&!n.is_infinite;
ensures \result .equals(this);

also

requires !this.is_infinite&&n.is_infinite;
ensures \result .equals(n);

also

requires this.is_infinite&&n.is_infinite;

{|

requires this.nonnegative == n.nonnegative;
ensures \result .equals(this);

also

requires this.nonnegative != n.nonnegative;
ensures \result .equals(new java.math.BigInteger("0"));

|}

also

requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.add(n.finite_value));

|}

subtract

public JMLInfiniteInteger subtract(JMLInfiniteInteger n)

Return the difference between this integer and the argument.

See Also:

JMLInfiniteInteger.add(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.negate()

Specifications: (class)pure

Specifications inherited from overridden method subtract(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
requires n != null;

{|

ensures \result != null;

also

requires this.is_infinite&&!n.is_infinite;
ensures \result .equals(this);

also

requires !this.is_infinite&&n.is_infinite;
ensures \result .equals(n.negate());

also

requires this.is_infinite&&n.is_infinite;

{|

requires this.nonnegative == n.nonnegative;
ensures \result .equals(new java.math.BigInteger("0"));

also

requires this.nonnegative != n.nonnegative;
ensures \result .equals(this);

|}

also

requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.subtract(n.finite_value));

|}

multiply

public JMLInfiniteInteger multiply(JMLInfiniteInteger n)

Return the product of this integer and the argument.

See Also:

JMLInfiniteInteger.divide(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.remainder(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.mod(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method multiply(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
requires n != null;

{|

ensures \result != null&&\result .sign == this.sign*n.sign;

also

requires this.equals(new java.math.BigInteger("0"))||n.equals(new java.math.BigInteger("0"));
ensures \result .equals(new java.math.BigInteger("0"));

also

requires !(this.equals(new java.math.BigInteger("0"))||n.equals(new java.math.BigInteger("0")));

{|

requires this.is_infinite||n.is_infinite;
ensures \result .is_infinite;

also

requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.multiply(n.finite_value));

|}

|}

divide

public JMLInfiniteInteger divide(JMLInfiniteInteger n)

Return the quotient of this integer divided by the argument.

See Also:

JMLInfiniteInteger.multiply(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.remainder(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.mod(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method divide(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
requires n != null&&n.sign != 0;

{|

ensures \result != null&&(\result .sign == 0||\result .sign == this.sign*n.sign);

also

requires this.is_infinite&&n.is_infinite;
ensures !\result .is_infinite&&\result .abs().equals(new java.math.BigInteger("1"));

also

requires this.is_infinite&&!n.is_infinite;
ensures \result .is_infinite;

also

requires !this.is_infinite&&n.is_infinite;
ensures \result .equals(new java.math.BigInteger("0"));

also

requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.divide(n.finite_value));

|}

     also

public exceptional_behavior
requires n != null&&n.sign == 0;
signals_only java.lang.ArithmeticException;

remainder

public JMLInfiniteInteger remainder(JMLInfiniteInteger n)

Return the remainder of this integer divided by the argument.

See Also:

JMLInfiniteInteger.divide(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.mod(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method remainder(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
requires n != null&&n.sign != 0;

{|

ensures \result != null;

also

requires this.is_infinite;
ensures \result .equals(new java.math.BigInteger("0"));

also

requires !this.is_infinite&&n.is_infinite;
ensures \result .abs().equals(this.abs());
ensures \result .sign == this.sign*n.sign;

also

requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.remainder(n.finite_value));

|}

     also

public exceptional_behavior
requires n != null&&n.sign == 0;
signals_only java.lang.ArithmeticException;

mod

public JMLInfiniteInteger mod(JMLInfiniteInteger n)
                       throws ArithmeticException

Return this integer modulo the argument.

Throws:

ArithmeticException

See Also:

JMLInfiniteInteger.divide(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.remainder(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method mod(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
requires n != null&&n.sign == 1;

{|

ensures \result != null&&\result .sign >= 0;

also

requires this.is_infinite;
ensures \result .equals(new java.math.BigInteger("0"));

also

requires !this.is_infinite&&n.is_infinite;
ensures \result .equals(n);

also

requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.mod(n.finite_value));

|}

     also

public exceptional_behavior
requires n != null&&n.sign != 1;
signals_only java.lang.ArithmeticException;

pow

public JMLInfiniteInteger pow(int n)

Return this integer raised to the argument's power.

Specifications: (class)pure

Specifications inherited from overridden method pow(int n) in interface JMLInfiniteInteger:
       non_null (class)pure

public normal_behavior
requires n >= 0;

{|

ensures \result != null&&(\result .nonnegative <==> n%2 == 0||this.nonnegative);

also

requires this.is_infinite;
ensures n != 0 ==> \result .is_infinite;
ensures n == 0 ==> !\result .is_infinite&&\result .finite_value.equals(new java.math.BigInteger("1"));

also

requires !this.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.pow(n));

|}

     also

public exceptional_behavior
requires n < 0;
signals_only java.lang.ArithmeticException;

doubleValue

public double doubleValue()

Return this integer approximated by a double.

See Also:

JMLInfiniteInteger.floatValue()

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (class)pure

public normal_behavior
requires this.is_infinite&&this.nonnegative;
ensures \result == Infinity;

     also

requires this.is_infinite&&!this.nonnegative;
ensures \result == -Infinity;

     also

requires !this.is_infinite;
ensures \result == this.finite_value.doubleValue();

floatValue

public float floatValue()

Return this integer approximated by a float.

See Also:

JMLInfiniteInteger.doubleValue()

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (class)pure

public normal_behavior
requires this.is_infinite&&this.nonnegative;
ensures \result == Infinity;

     also

requires this.is_infinite&&!this.nonnegative;
ensures \result == -Infinity;

     also

requires !this.is_infinite;
ensures \result == this.finite_value.floatValue();

toString

public String toString()

Return the decimal representation of this integer.

Specified by:

toString in interface JMLInfiniteInteger

Overrides:

toString in class Object

See Also:

JMLInfiniteInteger.toString(int)

Specifications: (class)pure

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (class)pure

     also

public normal_behavior
ensures \result .equals(this.toString(10));

toString

public String toString(int radix)

Return the digits representing this integer in the given radix.

See Also:

JMLInfiniteInteger.toString()

Specifications: (class)pure

Specifications inherited from overridden method toString(int radix) in interface JMLInfiniteInteger:
       (class)pure

public model_program { ... }

longValue

public long longValue()

Converts this BigInteger to a long

Specifications: (class)pure

intValue

public int intValue()

Converts this BigInteger to an integer

Specifications: (class)pure