2.3. Unbounded verification🔗

Bounded symbolic execution unrolls a loop a fixed number of times, so on its own it cannot prove a property for every run of a loop whose iteration count is not statically known. Loop invariants close that gap. A while loop may carry one or more invariant clauses, each an expression that must hold when the loop is first reached and be preserved by every iteration.

procedure countUp()
{
    var n: int := 5;
    var i: int := 0;
    while (i < n)
      invariant i >= 0
      invariant i <= n
    {
        i := i + 1
    };
    assert i == n
};

The invariants let Laurel replace the loop with three obligations that stand in for it no matter how many times it runs:

1. the invariants hold on entry to the loop;

2. assuming the invariants and the guard, one iteration of the body re-establishes the invariants;

3. after the loop, the invariants together with the negation of the guard may be assumed.

None of these obligations mentions a concrete iteration count, so an invariant strong enough to imply the property discharges it for an unbounded loop. Each invariant is checked independently and reports a failure against its own source range, so a diagnostic points at the specific invariant that does not hold rather than at the whole loop.