4.3. Loop invariants🔗

Laurel cannot know in advance how many times a loop runs, so it reasons about loops through a loop invariant: a condition that holds every time the loop guard is evaluated — on first entry and after each execution of the body.

A loop invariant serves two purposes. Inside the loop it tells Laurel what is true, which is what lets it prove that operations in the body are safe. After the loop it combines with the negated guard to describe the state on exit.

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

The two invariants together establish i == n after the loop: the loop exits when i < n is false, so i >= n, and the second invariant gives i <= n.

A loop invariant must hold on entry and be preserved by the body. If it fails on entry, Laurel reports the error at the offending invariant. For example, initializing i to -1 above would break invariant i >= 0 before the loop even starts, and that specific invariant is flagged.