4.7.1. While🔗

procedure whileLoop(n: int) returns (i: int)
  opaque
  ensures i >= 0
{
  i := 0;
  while (i < n)
    invariant 0 <= i
  {
    i := i + 1
  }
};

Invariants are optional as far as the grammar is concerned; they are what verification needs, and are covered under Loop invariants.

Keep the loop condition pure. An effectful condition is currently evaluated once before the loop rather than at every iteration, and a field access in it may evaluate its receiver more than once, or, when it stores, after the stored value, so that a check depending on the receiver's effect can verify wrongly. Hoist the effect yourself and update a plain variable in the body.

4.7.2. For🔗

procedure forLoop(n: int) returns (sum: int)
  opaque
{
  sum := 0;
  for (var i: int := 0; i < n; i := i + 1)
    invariant 0 <= i
  {
    sum := sum + i
  }
};

A for is desugared immediately into its initializer followed by a while whose body ends with the step, so everything true of while is true of it.

4.7.3. Do-while🔗

procedure doWhileLoop() returns (x: int)
  opaque
{
  x := 0;
  do {
    x := x + 1
  } while (x < 3)
    invariant 0 <= x
};

The body runs at least once. Invariants are still checked at the loop head, including before the first execution of the body.

4.7.4. Labels and exits🔗

A block may carry a label, and exit jumps to the end of the enclosing block with that label. The label must be in lexical scope.

procedure labelledExit(done: bool) returns (x: int)
  opaque
{
  x := 1;
  {
    if done then { exit finished };
    x := 2
  } finished
};

Laurel has no break or continue keyword: a labelled block plus exit is how a front end builds them — break exits a block wrapped around the loop, continue exits a block wrapped around the loop body. Code following an unconditional return, exit or goto in the same block is reported as dead.

goto jumps back to the start of the enclosing block with that label, which makes the block a loop. Such a block may carry invariants, written after its label like a while loop's; they are checked on entry and on every goto back to the start. A block that no goto targets checks them once, on entry.

procedure countUp() returns (i: int)
  opaque
  ensures i == 3
{
  i := 0;
  {
    i := i + 1;
    if i < 3 then { goto again }
  } again
    invariant 0 <= i && i <= 2
};

Because a goto can only target an enclosing block, the control flow stays reducible: the RestructureGotos pass lowers each block that some goto targets to a while (true) loop before translation to Core, so a front end that emits unstructured jumps — a bytecode front end, say — does not need to recover loops itself.