`while` Loop

The while loop repeatedly executes a block while a boolean condition holds.

Surface Syntax#

Minimal form:

while <condition> {
  // body
}

<condition> is an expression. Parentheses are optional because the condition is parsed using the normal expression grammar:

while (x < y && y < 10) {
  ...
}

`while let` (Pattern-Destructuring Loop Form)#

Silk supports a while let loop form for iterating while a refutable pattern matches:

while let <pattern> = <scrutinee> {
  ...
}

while let mut <pattern> = <scrutinee> {
  ...
}

Notes:

The scrutinee expression is evaluated once per iteration.
The pattern binders (for example Some(v) binds v) are in scope only in the loop body.
while let mut marks binders introduced by the pattern as mutable for that iteration's loop body.
The loop exits when the scrutinee does not match the pattern.
Supported patterns are the same as if let (see flow if else).

`while let` chains (`&& let`)#

The while let loop form supports the same short-circuiting && chain syntax as if let, mixing refutable let clauses and ordinary boolean clauses:

fn main () -> int {
  var x: int? = Some(3);
  var sum: int = 0;

  while let mut Some(v) = x && v > 0 {
    let original = v;
    v = v + 1;
    sum = sum + v;
    x = if original <= 1 { None } else { Some(original - 1) };
  }

  return sum;
}

Semantics:

Clauses are evaluated left-to-right and short-circuit like &&.
let clause binders are in scope for subsequent clauses and for the loop body, but they do not escape the loop.
let mut clauses introduce mutable binders for subsequent clauses and for that iteration's loop body.
let move clauses consume their scrutinee for ownership-tracked values. This is most useful when the scrutinee is a fresh expression each iteration, such as while let move Some(value) = next() { ... }; a moved local source binding is unavailable to later clauses, the loop body, and code after the loop.
The loop exits when any clause fails (pattern mismatch or boolean false).

Parsing note (Supported forms):

&& at the top level is parsed as a clause separator. Use parentheses if a clause needs its own && / || / ?? expression at the top level.

Example (optional countdown):

fn main () -> int {
  var x: int? = Some(3);
  var sum: int = 0;

  while let Some(v) = x {
    sum = sum + v;
    if v <= 1 {
      x = None;
    } else {
      x = Some(v - 1);
    }
  }

  // 3 + 2 + 1 = 6
  return sum;
}

Loop Specifications (`#invariant` / `#variant` / `#monovariant`)#

The language supports attaching loop specifications immediately before a while. This is part of Formal Silk (see formal verification). When Formal Silk syntax is present, the compiler proves these obligations with Z3 at compile time.

#invariant <expr>;
#variant <expr>;
#monovariant <expr>;
while <condition> {
  ...
}

Semantics#

Evaluation rules:

The condition is evaluated before each iteration.
If the condition evaluates to true, the body block executes.
After the body completes normally, control returns to the condition.
If the condition evaluates to false, the loop terminates and execution continues after the loop statement.

Control-flow statements inside the body follow their own definitions:

break exits the nearest enclosing loop (flow break).
continue skips to the next iteration (flow continue).
return exits the function (flow return).
panic exits the function via the typed error system (typed errors).

Blocks create scopes. A let declared inside the body is not visible outside the loop’s body block.

Type Checking Rules#

The checker enforces:

The loop condition must have type bool (otherwise E2001).
Each #invariant expression must have type bool (otherwise E2001).
If present, the #variant expression must have an integer type (int or a fixed-width integer; otherwise E2001).
Each #monovariant expression must have an integer type (int or a fixed-width integer; otherwise E2001).

#invariant, #variant, and #monovariant expressions are compile-time-only (erased from runtime code). When Formal Silk verification is enabled by syntax, they are proved with Z3 during compilation.

Examples#

Minimal loop with `break`#

fn main () -> int {
  while true {
    break;
  }
  return 0;
}

Loop with invariants and a variant#

fn main () -> int {
  let limit: int = 3;
  #const original_limit = limit;

  let mut i: int = 0;
  #invariant i >= 0;
  #invariant i <= original_limit;
  #variant original_limit - i;
  while i < limit {
    i = i + 1;
  }

  return 0;
}

Notes#

Supported forms:

while loops with boolean conditions.
while let <pattern> = <expr> { ... } pattern-destructuring loops.
&& let-chains in while let loop conditions.
break / continue inside while bodies.
#invariant (type-checked as bool), #variant (type-checked as an integer), and #monovariant (type-checked as an integer) attached to while.

examples:

while Loop