\bigint is the type of unbounded, mathematical integers. Most typically when writing specifications, users think in terms in mathematical integers and the limitations of fixed bit-widths are an afterthought. Mathematical integers are also easier for solvers to reason about, so using them is natural in writing specifications. They are similar to Java’s BigInteger, except that no actual computation is being done, only logical reasoning.

Since \bigint is a JML built-in type, it may only be used within specifications. But that includes using it as the type of ghost fields, ghost variables and the parameters and result types of model methods.

The \bigint built-in type is intuitive and natural to use, but for the sake of clarity, its operations are listed here. j and k are two values of type \bigint and i a value of a Java numeric type.

  • j == k and j != k mean equality and inequality
  • - j is mathematical integer negation
  • j + k is mathematical integer addition
  • j - k is mathematical integer subtraction
  • j * k is mathematical integer multiplication
  • j / k is mathematical integer division (truncation toward zero); k must not be 0; j/k is negative or zero if j and k have different signs and is positive or zero if j and k have the same sign
  • j % k is mathematical integer modulo, but is similar to Java’s % operation: k may not be zero, j%k has the same sign as j and is independent of the sign of k, and for k != 0, (j/k)*k + (j%k) == j
  • < and <= and > and >= have their expected meanings with the result type being boolean
  • casts are allowed to and from other numeric types, such as (\bigint)i or (int)j. When casting from \bigint to a bounded type, a range check is performed, depending on the arithmetic mode.

For example, one can write the following:

int k;
//@ ghost \bigint i; // ghost variables are specification only
//@ set i = Integer.MAX_VALUE;
//@ set i = i * i; // would overflow 32-bit int
//@ set i = (i+i)/i;

The Java java.lang.Math class defines a number of functions on integer types. The specifications of model methods for corresponding functions on bigints are also included in OpenJML (and more may be added):

// openjml --esc Bigint.java
public class Bigint {

  //@ ghost \bigint x;
  //@ ghost \bigint y;

  public void test() {
    //@ assert Math.abs(x) >= 0;
    //@ assert x != 0 && y != 0 ==> Math.gcd(x,y) > 0;
  }
}