Contracts

When your code calls a method whose body is large or already proven, you don’t have to drag that body into every proof. Give the method a contract and reason against the contract instead. This is assume-guarantee: the callee is proven to keep its promise once, and every caller assumes it.

Contracts are only sound for pure methods (no side effects, value returning), and a contract is only trusted once its own enforce-proof is green, which the tooling runs for you.

Predicates, not strings

A contract names a static boolean predicate rather than a string expression, so it stays ordinary type-checked code the engine can analyze. @Requires is the precondition over the parameters; @Ensures is the postcondition over the result and the parameters.

@Requires("nonNegative")
@Ensures("resultNonNegative")
static int isqrt(int n) { ... }

static boolean nonNegative(int n) { return n >= 0; }
static boolean resultNonNegative(int result, int n) { return result >= 0; }

From that, two directions are derived: enforce (assume the precondition, run the body, assert the postcondition) and replace (at a call site, assert the precondition, then take a nondet result that satisfies the postcondition).

Keeping contracts out of production code

You usually don’t want bmc4j annotations in src/main. Put the contract on a test-side interface that mirrors the method’s signature and holds the predicates, marked @BmcContractsFor(Target::class):

// src/main, plain
public final class Triangle {
    public static int triangle(int n) { int s = 0; for (int i = 1; i <= n; i++) s += i; return s; }
}

// src/test, the contract lives here
@BmcContractsFor(Triangle.class)
interface TriangleContract {
    @Requires("bounded") @Ensures("nonNeg") int triangle(int n);
    static boolean bounded(int n)            { return n >= 0 && n <= 8; }
    static boolean nonNeg(int result, int n) { return result >= 0; }
}

@ExpectEnforce(...) sets the expected verdict of the enforce-proof, the same way expect works on a proof.