JML Tutorial - Arithmetic and Arithmetic Modes

If you have tried verifying some programs of your own that involve arithmetic, you will likely have encountered arithmetic overflow errors. This lesson describes how to specify arithmetic modes to prevent those errors.

Integer arithmetic in Java code is 2’s-complement arithmetic, modulo 32- or 64- bits (for int or long), with values sometimes being truncated to only 16 or 8 bits (for types short or char). Java’s arithmetic is defined to give no warning if arithmetic operations overflow or underflow or if conversions lose high-order bits. Thus in Java, for an int x (or long x), x+1 is not necessarily larger than x. Programmers using Java often ignore the possibility of such overflows, informally reasoning that in the intended use of the program no numbers large enough to cause overflow will be used. However, one purpose of specification and verification is to document the precise conditions under which a program behaves as expected.

JML is designed to, by default, warn about potential overflows in Java code. Although JML takes the position that such overflows indicate a possible bug, that is not always the case. For example, code that generates psuedo-random numbers or performs encryption or compression often intentionally uses overflow. But such uses are less common.

On the other hand, readers of specifications generally interpret expressions mathematically—that is, readers interpret specifications as using mathematical (i.e., infinite precision) arithmetic.¹

Consequently, JML defines three arithmetic modes (for integer arithmetic):

• Java mode: arithmetic behaves precisely as in Java, with silent wrap-around of overflowing and underflowing operations, which are not considered errors,
• Safe mode: the results of arithmetic operations are the same as in Java mode, but verification errors are issued if the operation may over/underflow
• Math (bigint) mode: Values and operations are the same as in mathematics—values are unbounded and so there is no over/underflow.

The default in JML is to use safe mode for expressions in Java code but math mode (i.e., bigint mode) for expressions in specifications. (We describe several ways to specify the arithmetic mode to be used below.)

First an example. The following simple code

// openjml --esc T_arithmetic1.java
public class T_arithmetic1 {
  public int increment(int i) {
    int new_i = i+1;   // ERROR: may overflow!
    //@ assert new_i == i+1;   // ERROR: may fail!
    return new_i;
  }
}

produces several errors:

T_arithmetic1.java:5: verify: The prover cannot establish an assertion (Assert) in method increment
    //@ assert new_i == i+1;   // ERROR: may fail!
        ^
T_arithmetic1.java:4: verify: The prover cannot establish an assertion (ArithmeticOperationRange) in method increment: overflow in int sum
    int new_i = i+1;   // ERROR: may overflow!
                 ^
2 verification failures

To avoid these overflow errors, one can use an assumption (or a precondition) to guard against the potential overflow. The following thus verifies without error.

// openjml --esc T_arithmetic2.java
public class T_arithmetic2 {
  public int increment(int i) {
    //@ assume i < Integer.MAX_VALUE;
    int new_i = i+1;
    //@ assert new_i == i+1;
    return new_i;
  }
}

Similarly

// openjml --esc T_arithmetic3.java
public class T_arithmetic3 {
  public int abs(int i) {
      if (0 <= i) {
          return i;
      } else {
          //@ assert -i > 0;
          return -i;   // ERROR: see text!
      }
  }
}

produces the following errors (because Integer.MIN_VALUE has no positive counterpart in the 2’s-complement integer representation used by Java).

T_arithmetic3.java:8: verify: The prover cannot establish an assertion (ArithmeticOperationRange) in method abs: int negation
          return -i;   // ERROR: see text!
                 ^
1 verification failure

However, the following verifies without error, due to the added assumption (which might be recorded as a precondition) that guards against the potential overflow.

// openjml --esc T_arithmetic4.java
public class T_arithmetic4 {
  public int abs(int i) {
      //@ assume i != Integer.MIN_VALUE;
      if (0 <= i) {
          return i;
      } else {
          //@ assert -i > 0;
          return -i;
      }
  }
}

Overflows in Intermediate Computations

One final example is a bug that was present in Java’s binary search library code for years.² The binary search algorithm requires computing a value mid that is midway between low and hi, which are indices into an array. The simple computation mid = (lo+hi)/2; has a potential overflow problem, and OpenJML would issue an error for the potential overflow; however, the alternative mid = lo + (hi-lo)/2; does not have that potential overflow. We will elaborate this example when discussing specifying and verifying loops in a later lesson.

Design Alternatives

An alternate design of JML would have the default mode for specification and Java code both be Java mode. But this would hide bugs, since if the potential overflow in the Java code is missed, it likely would be missed also in the specification, as in the first example above. JML’s defaults are chosen to highlight potential overflow bugs.

Setting the Arithmetic Mode

There are a variety of ways to set the arithmetic mode in JML:

• Within a specification expression, subexpressions can be computed with a specific arithmetic mode using the functions \java_math(...), \safe_math(...), or \bigint_math(...). These functions each take one argument and return the value of the argument, but the argument expression is computed using the given mode. These operations are not available for Java code, because there are no such operations in Java. (In Java one could use the type BigInteger to obtain arbitrary precision integer computations, but there is no built-in way to receive warnings about overflows like JML’s safe-math mode.)
• The mode for a proof attempt using OpenJML can be set using command-line options: --code-math=... and --spec-math=... to set the mode for Java code and specifications, respectively, with possible values of java, safe, and bigint. For example, to turn off overflow warnings in the Java code one can set the global default using --code-math=java
• You can set the mode for a particular method using the modifiers code_java_math, spec_java_math, code_safe_math, spec_safe_math and spec_bigint_math (note that there is no such thing as code_bigint_math, since that would change the meaning of the Java code).

In the following example, both the code and specs are computed with Java math, so they agree, even when there is an overflow; thus this example verifies.

// openjml --esc T_arithmetic5.java
public class T_arithmetic5 {
  //@ code_java_math
  public int inc_as_in_java(int i) { 
    int new_i = i+1;
    //@ assert new_i == \java_math(i+1);
    return new_i;
  }
}

Exercises

Follow the link in the above heading to work on the exercises on this topic.

Resources

• T_arithmetic1 file
• T_arithmetic2 file
• T_arithmetic3 file
• T_arithmetic4 file
• T_arithmetic5 file

Footnotes