Invariants and contracts

A loop may carry an invariant: a fact that must hold before the first iteration (the entry obligation) and after every back-edge (the back-edge obligation). Invariants connect the loop family to Nitpick's Design by Contract surfaces — see also the Design by Contract cookbook.

Syntax

Place invariant <expr> between the loop header and the body:

func:failsafe = int32(tbb32:err) {
    exit 1;
};

func:main = int32() {
    int32:sum = 0i32;
    loop(0i32, 5i32, 1i32) invariant sum >= 0i32 {
        sum += $;
    }
    exit sum;
};

while loops take an invariant the same way:

while (i < n) invariant i <= n {
    i += 1i32;
}

Entry vs back-edge

• The entry check runs once, before the first iteration — even when the loop body runs zero times.
• The back-edge check runs after each iteration completes and control loops around (the condition re-check or the counter step).

Interaction with break and continue

• break leaves the loop before the back-edge, so it skips the back-edge invariant check for the exiting iteration.
• continue jumps to the back-edge, so it is still subject to the back-edge invariant check.

// continue still hits the back-edge: the invariant must hold there.
while (i < n) invariant i <= bound {
    if (special(i)) { i += 1i32; continue; }   // checked
    i += 1i32;
}

If a continue pushes the loop variable past what the invariant allows, the back-edge check fails. Under --debug-contracts this surfaces at runtime as a Result error and the program exits with code 48 (regression bug907).

Checking modes

Two flags drive invariant checking:

• --verify-contracts asks Z3 to discharge the entry and back-edge obligations at compile time. A loop with a break is handled correctly: Z3 proves the invariant for the paths that actually reach the back-edge (regression bug906).
• --debug-contracts inserts runtime checks. A violated invariant yields a Result error, routed to the failsafe path with exit code 48.

Add --debug-z3 to dump the solver queries when diagnosing a --verify-contracts outcome.

Purity

Invariant expressions are read-only predicates over loop state. Keep them free of side effects; they describe the loop, they do not drive it.

Cycle note (v0.38.8)

The v0.38.8 cycle fixed a PHI-node mismatch that rejected counted-loop invariants reading $ under --debug-contracts (bug905), and verified the break/continue interactions above across both checking modes (bug903, bug904, bug906, bug907).

Back to the cookbook index.