java.math
Class BigInteger

java.lang.Object
  java.lang.Number
      java.math.BigInteger

All Implemented Interfaces:

Comparable, Serializable

public class BigInteger

extends Number

implements Comparable

JML's specification of java.math.BigInteger.

Version:

$Revision: 1.24 $

Author:

David R. Cok, Gary T. Leavens

Class Specifications

public invariant this.sign == this.compareTo(java.math.BigInteger.ZERO); public invariant java.math.BigInteger.ZERO != null&&java.math.BigInteger.ZERO.equals(valueOf(0)); public invariant java.math.BigInteger.ZERO.equals(java.math.BigInteger.ZERO); public invariant java.math.BigInteger.ONE != null&&java.math.BigInteger.ONE.equals(valueOf(1)); public invariant java.math.BigInteger.ONE.equals(java.math.BigInteger.ONE); public invariant !java.math.BigInteger.ZERO.equals(java.math.BigInteger.ONE); public constraint java.math.BigInteger.ZERO == \old(java.math.BigInteger.ZERO); public constraint java.math.BigInteger.ONE == \old(java.math.BigInteger.ONE); public represents sign <- this.signum();

Specifications inherited from class Object

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

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
int	sign
\bigint	value

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
(package private) static int[]	bnExpModThreshTable
(package private)  int[]	mag
static BigInteger	ONE
(package private)  int	signum
(package private) static byte[]	trailingZeroTable
static BigInteger	ZERO

 

Model Constructor Summary

BigInteger(\bigint val)

 

Constructor Summary
	BigInteger(non_null byte[] val)
(package private)	BigInteger(char[] val)
	BigInteger(int signum, non_null byte[] magnitude)
	BigInteger(int bitLength, int certainty, Random rnd)
	BigInteger(int numBits, Random rnd)
	BigInteger(String val)
	BigInteger(String val, int radix)

 

Model Method Summary
static BigInteger	convert(byte[] val)
static BigInteger	parse(String val, int radix)

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

 

Method Summary
BigInteger	abs()
BigInteger	add(BigInteger val)
(package private) static int	addOne(int[] a, int offset, int mlen, int carry)
BigInteger	and(BigInteger val)
BigInteger	andNot(BigInteger val)
(package private) static int	bitCnt(int val)
int	bitCount()
(package private) static int	bitLen(int w)
int	bitLength()
BigInteger	clearBit(int n)
int	compareTo(non_null Object o)
int	compareTo(non_null BigInteger val)
BigInteger	divide(BigInteger val)
BigInteger[]	divideAndRemainder(BigInteger val)
double	doubleValue()
boolean	equals(nullable Object x)
BigInteger	flipBit(int n)
float	floatValue()
BigInteger	gcd(BigInteger val)
int	getLowestSetBit()
int	hashCode()
int	intValue()
boolean	isProbablePrime(int certainty)
(package private)  int	jacobiSymbol(int p, BigInteger n)
(package private)  int[]	javaIncrement(int[] val)
long	longValue()
BigInteger	max(BigInteger val)
BigInteger	min(BigInteger val)
BigInteger	mod(BigInteger m)
BigInteger	modInverse(BigInteger m)
BigInteger	modPow(BigInteger exponent, BigInteger m)
(package private) static int	mulAdd(int[] out, int[] in, int offset, int len, int k)
BigInteger	multiply(BigInteger val)
BigInteger	negate()
BigInteger	not()
BigInteger	or(BigInteger val)
BigInteger	pow(int exponent)
(package private)  boolean	primeToCertainty(int certainty)
(package private) static void	primitiveLeftShift(int[] a, int len, int n)
(package private) static void	primitiveRightShift(int[] a, int len, int n)
static BigInteger	probablePrime(int bitLength, Random rnd)
BigInteger	remainder(BigInteger val)
BigInteger	setBit(int n)
BigInteger	shiftLeft(int n)
BigInteger	shiftRight(int n)
int	signum()
BigInteger	subtract(BigInteger val)
boolean	testBit(int n)
byte[]	toByteArray()
String	toString()
String	toString(int radix)
(package private) static int	trailingZeroCnt(int val)
static BigInteger	valueOf(long val)
BigInteger	xor(BigInteger val)

 

Methods inherited from class java.lang.Number

byteValue, shortValue

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

value

public \bigint value

sign

public int sign

signum

int signum

mag

int[] mag

ZERO

public static final BigInteger ZERO

ONE

public static final BigInteger ONE

bnExpModThreshTable

static int[] bnExpModThreshTable

trailingZeroTable

static final byte[] trailingZeroTable

BigInteger

public BigInteger(\bigint val)

Specifications: (class)pure

BigInteger

public BigInteger(non_null byte[] val)

Specifications: (class)pure

public normal_behavior
requires val != null;
requires val.length != 0;

     also

public exceptional_behavior
requires val != null;
requires val.length == 0;
signals_only java.lang.NumberFormatException;

     also

public exceptional_behavior
requires val == null;
signals_only java.lang.NullPointerException;

BigInteger

public BigInteger(int signum,
                  non_null byte[] magnitude)

Specifications: (class)pure

public normal_behavior
requires magnitude != null;
requires signum == 0||signum == 1||signum == -1;
requires signum == 0 <==> convert(magnitude).equals(java.math.BigInteger.ZERO);
ensures this.sign == signum;

BigInteger

public BigInteger(String val,
                  int radix)

Specifications: (class)pure

public normal_behavior
requires val != null&&!val.equals("");
requires radix > 1;
ensures this.equals(parse(val,radix));

     also

public exceptional_behavior
requires val != null&&val.equals("");
signals_only java.lang.NumberFormatException;

     also

public exceptional_behavior
requires val == null;
signals_only java.lang.NullPointerException;

BigInteger

BigInteger(char[] val)

Specifications: (class)pure

normal_behavior
ensures true;

BigInteger

public BigInteger(String val)

Specifications: (class)pure

public normal_behavior
requires val != null&&!val.equals("");
ensures this.equals(parse(val,10));

     also

public exceptional_behavior
requires val.equals("");
signals_only java.lang.NumberFormatException;

     also

public exceptional_behavior
requires val == null;
signals_only java.lang.NullPointerException;

BigInteger

public BigInteger(int numBits,
                  Random rnd)

Specifications: (class)pure

BigInteger

public BigInteger(int bitLength,
                  int certainty,
                  Random rnd)

Specifications: (class)pure

parse

public static BigInteger parse(String val,
                               int radix)

Specifications: pure

convert

public static BigInteger convert(byte[] val)

Specifications: pure

probablePrime

public static BigInteger probablePrime(int bitLength,
                                       Random rnd)

Specifications: pure

primeToCertainty

boolean primeToCertainty(int certainty)

Specifications: (class)pure

jacobiSymbol

int jacobiSymbol(int p,
                 BigInteger n)

Specifications: (class)pure

valueOf

public static BigInteger valueOf(long val)

Specifications: pure

add

public BigInteger add(BigInteger val)

Specifications: (class)pure

requires val != null;

subtract

public BigInteger subtract(BigInteger val)

Specifications: (class)pure

requires val != null;
ensures this.equals(\result .add(val));

multiply

public BigInteger multiply(BigInteger val)

Specifications: (class)pure

requires val != null;

divide

public BigInteger divide(BigInteger val)

Specifications: (class)pure

requires val != null;
ensures this.equals(\result .multiply(val).add(this.remainder(val)));

divideAndRemainder

public BigInteger[] divideAndRemainder(BigInteger val)

Specifications: (class)pure

ensures \result [0].equals(this.divide(val));
ensures \result [1].equals(this.remainder(val));

remainder

public BigInteger remainder(BigInteger val)

Specifications: (class)pure

pow

public BigInteger pow(int exponent)

Specifications: (class)pure

gcd

public BigInteger gcd(BigInteger val)

Specifications: (class)pure

primitiveRightShift

static void primitiveRightShift(int[] a,
                                int len,
                                int n)

Specifications: (class)pure

primitiveLeftShift

static void primitiveLeftShift(int[] a,
                               int len,
                               int n)

Specifications: (class)pure

abs

public BigInteger abs()

Specifications: (class)pure

assignable \nothing;
ensures \result .signum() >= 0&&(this.sign == 0 ==> \result .signum() == 0);

negate

public BigInteger negate()

Specifications: (class)pure

assignable \nothing;
ensures \result .signum() == -this.sign;

signum

public int signum()

Specifications: (class)pure

ensures \result == this.sign;

mod

public BigInteger mod(BigInteger m)

Specifications: (class)pure

modPow

public BigInteger modPow(BigInteger exponent,
                         BigInteger m)

Specifications: (class)pure

mulAdd

static int mulAdd(int[] out,
                  int[] in,
                  int offset,
                  int len,
                  int k)

Specifications: (class)pure

addOne

static int addOne(int[] a,
                  int offset,
                  int mlen,
                  int carry)

Specifications: (class)pure

modInverse

public BigInteger modInverse(BigInteger m)

Specifications: (class)pure

shiftLeft

public BigInteger shiftLeft(int n)

Specifications: (class)pure

shiftRight

public BigInteger shiftRight(int n)

Specifications: (class)pure

javaIncrement

int[] javaIncrement(int[] val)

Specifications: (class)pure

and

public BigInteger and(BigInteger val)

Specifications: (class)pure

or

public BigInteger or(BigInteger val)

Specifications: (class)pure

xor

public BigInteger xor(BigInteger val)

Specifications: (class)pure

not

public BigInteger not()

Specifications: (class)pure

andNot

public BigInteger andNot(BigInteger val)

Specifications: (class)pure

testBit

public boolean testBit(int n)

Specifications: (class)pure

setBit

public BigInteger setBit(int n)

Specifications: (class)pure

clearBit

public BigInteger clearBit(int n)

Specifications: (class)pure

flipBit

public BigInteger flipBit(int n)

Specifications: (class)pure

getLowestSetBit

public int getLowestSetBit()

Specifications: (class)pure

bitLength

public int bitLength()

Specifications: (class)pure

bitLen

static int bitLen(int w)

Specifications: (class)pure

bitCount

public int bitCount()

Specifications: (class)pure

bitCnt

static int bitCnt(int val)

Specifications: (class)pure

trailingZeroCnt

static int trailingZeroCnt(int val)

Specifications: (class)pure

isProbablePrime

public boolean isProbablePrime(int certainty)

Specifications: (class)pure

compareTo

public int compareTo(non_null BigInteger val)

Specifications: (class)pure

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)

Specified by:

compareTo in interface Comparable

Specifications: (class)pure

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

equals

public boolean equals(nullable Object x)

Overrides:

equals in class Object

Specifications: pure

     also

public normal_behavior
requires x != null&&x instanceof java.math.BigInteger;
assignable \nothing;
ensures \result == x.equals(this);

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

min

public BigInteger min(BigInteger val)

Specifications: (class)pure

max

public BigInteger max(BigInteger val)

Specifications: (class)pure

hashCode

public int hashCode()

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;

toString

public String toString(int radix)

Specifications: (class)pure

ensures \result != null;
ensures parse(\result ,radix).equals(this);

toString

public String toString()

Overrides:

toString in class Object

Specifications: (class)pure

     also

ensures \result != null;
ensures parse(\result ,10).equals(this);

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;

toByteArray

public byte[] toByteArray()

Specifications: (class)pure

ensures convert(\result ).equals(this);
ensures_redundantly this.equals(\old(this));

intValue

public int intValue()

Specifications: (class)pure

     also

ensures_redundantly this.equals(\old(this));

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an int approximation to the value of this object *);

longValue

public long longValue()

Specifications: (class)pure

     also

ensures_redundantly this.equals(\old(this));

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an long approximation to the value of this object *);

floatValue

public float floatValue()

Specifications: (class)pure

     also

ensures_redundantly this.equals(\old(this));

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an float approximation to the value of this object *);

doubleValue

public double doubleValue()

Specifications: (class)pure

     also

ensures_redundantly this.equals(\old(this));

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an double approximation to the value of this object *);