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, so 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 or exit in the same block is reported as dead.