Integers

This section explain how prove properties about integers in Java code.

Nat

The annotation @Nat can be used to tell JVerify that an integer is never negative. Example:

int factorial(@Nat int n) {
    if (n == 0) {
        return 1;
    } else {
        return factorial(n - 1); // pass
    }
}

Without the @Nat annotation, JVerify would not have been able to prove termination, and indeed the program does not terminate if n is smaller than zero. Instead of @Nat, we could also have used precondition(n >= 0), but that is more verbose.

Bounded numbers

The types byte, int, short and long in Java are bounded. The values of these numbers all have lower and upper bounds, and doing arithmetic operations that cause these numbers to surpass these bounds, called an overflow, generally causes undesired results.

JVerify will check that any arithmetic operations on bounded numbers will not overflow. Example:

int triple(int x) {
  return 3 * x; // error: returned value may not be within the bounds of 'int'    
} 

You can let JVerify know no such overflow occurs by bounding the provided values:

int triple(int x) {
  precondition(3 * x < Integer.MAX_VALUE);
  
  return 3 * x; // pass    
} 

Unbounded numbers

Using the annotation @Unbounded, you can annotate integer types so JVerify will allow them to have unbounded values. Example:

@Erased
@Unbounded int triple(int x) {
  return 3 * x; // pass    
}

Note that the @Unbounded annotation can only be used in erased code. It is often useful in specifications, because working with unbounded numbers is easier, and since specifications are erased, they can use them.

Combining the above

Here follows an example that uses unbounded numbers is its specification, bounded numbers in the implementation, and natural numbers in both. It shows how each of these concepts is useful:

package org.strata.jverify.examples;

import static org.strata.jverify.JVerify.*;
import org.strata.jverify.*;

class Fibonacci {
    @Pure
    @Erased
    static @Unbounded @Nat int spec(@Unbounded @Nat int n) {
        return n < 2 ? n : spec(n - 1) + spec(n - 2);
    }

    public static @Nat int implementation(@Nat int n)
    {
        postcondition((int result) -> result == spec(n));
        
        // this precondition prevents overflow later in this method
        precondition(spec(n) <= Integer.MAX_VALUE);

        if (n == 0) {
            return 0;
        }

        int previousResult = 0;
        int result = 1;
        int i = 1;
        while(i < n)
        {
            invariant(result == spec(i));
            invariant(previousResult == spec(i - 1));
            invariant(i <= n);

            i = i + 1;

            // Using the precondition that the final result fits in an int32
            // And the knowledge that the intermediate results are smaller than the result
            // We can show the addition always fits in an int32
            SpecIsIncreasing(i, n);
            int addition = result + previousResult;
            previousResult = result;
            result = addition;
        }
        return result;
    }

    /**
     * Proves that Fibonacci numbers increase in value with increading input value
     */
    @Erased
    static void SpecIsIncreasing(@Unbounded @Nat int i, @Unbounded @Nat int j)
    {
        precondition(i <= j);
        postcondition(spec(i) <= spec(j));

        @Unbounded @Nat int x = i;
        while(x < j)
        {
            invariant(x <= j);
            invariant(spec(i) <= spec(x));
            x = x + 1;
        }
    }
}