Why can't I call get() in a do-while body when the trailing while condition checks the Optional?

← Safe Value Access · Ref: Q1379

No. A do/while checks its condition AFTER the body has already run, so the trailing 'while' cannot make anything in the body safe. Writing 'do ... while maybeName?' gives E08030 on the get() inside the body, and that is correct - by the time the check runs, the unsafe call has already happened.

WHY THE TRAILING CONDITION CANNOT HELP

Safe access works by proving the check happens BEFORE the access. A leading 'while maybeName?' checks first, so the body is safe. A do/while inverts that order:

  do
    stdout.println(maybeName.get())   //E08030 - runs BEFORE the check
  while maybeName?

The condition still controls whether you iterate again; it just cannot retroactively guarantee the first pass.

THREE WAYS THAT DO WORK

1. Guard from outside with 'if':

  if maybeName?
    do
      stdout.println(maybeName.get())
      loopDone: true
    while not loopDone

2. Use a PRE-FLOW guard on the 'do' itself. It sits between 'do' and the body, so it is evaluated first:

  do maybeName <- lookupName()
    stdout.println(maybeName.get())
    loopDone: true
  while not loopDone

3. Use a leading 'while' instead, if the loop does not need to run at least once:

  while maybeName?
    stdout.println(maybeName.get())

A PRE-FLOW GUARD OVERRIDES THE AT-LEAST-ONCE RULE

This surprises people. A do/while normally runs its body at least once, but a pre-flow guard is a real guard - if the value is unset the body runs ZERO times:

  do maybeName <- lookupMissingName()
    stdout.println("never printed")
  while not loopDone

The guard is a precondition on entering the loop at all, not part of the continuation condition.

WHICH CONDITIONS THE COMPILER CAN ANALYSE

Only a simple is-set check, or several combined with 'and':

  while maybeName? and stillGoing        //analysed - body is safe
  while maybeName? and not loopDone      //NOT analysed - E08030
  while maybeName? or useDefault         //NOT analysed - E08030

'or' genuinely breaks the guarantee. 'not' is refused conservatively: the analysis bails on the whole expression rather than reason about negation. If you hit this, hoist the check into an enclosing 'if' or a pre-flow guard.

DO NOT REASSIGN THE GUARDED VARIABLE

Inside a scope made safe by a check, reassigning that variable is E08040. The guarantee was established once; letting you overwrite it would invalidate it.

See Q67 for do-while basics. See Q163 for unwrapping Optional. See Q165 for why there is no unchecked get. See Q166 for the consistent safe-access pattern.

Example

defines module qa.safeaccess.dowhiletrailing

  defines function

    <?-
      Returns a set Optional.
    -?>
    lookupName() as pure
      <- rtn <- Optional("Steve")

    <?-
      Returns an unset Optional, to show a pre-flow guard refusing to enter the loop.
    -?>
    lookupMissingName() as pure
      <- rtn as Optional of String: Optional() of String

  defines program

    DoWhileSafeAccessDemo()
      stdout <- Stdout()

      // === GUARD FROM OUTSIDE WITH 'if' ===
      // The check runs before the loop, so the body is safe.

      outerName <- lookupName()
      outerDone <- false
      if outerName?
        do
          stdout.println(`Outer if guard: ${outerName.get()}`)
          outerDone: true
        while not outerDone

      // === PRE-FLOW GUARD ON THE 'do' ITSELF ===
      // Sits between 'do' and the body, so it is evaluated first.

      preFlowDone <- false
      do preFlowName <- lookupName()
        stdout.println(`Pre-flow guard: ${preFlowName.get()}`)
        preFlowDone: true
      while not preFlowDone

      // === A PRE-FLOW GUARD OVERRIDES THE AT-LEAST-ONCE RULE ===
      // The Optional is unset, so the body runs ZERO times.

      skippedDone <- false
      do missingName <- lookupMissingName()
        stdout.println(`Never printed: ${missingName.get()}`)
        skippedDone: true
      while not skippedDone
      stdout.println("Unset pre-flow guard skipped the body entirely")

      // === A LEADING 'while' CAN MAKE THE BODY SAFE ===
      // Checked before each iteration, so the ordering requirement is met.
      // 'and' composes; 'not' or 'or' would make the expression unanalysable.

      leadingName <- lookupName()
      stillGoing <- true
      while leadingName? and stillGoing
        stdout.println(`Leading while: ${leadingName.get()}`)
        stillGoing: false

Common mistakes

E08030 — The trailing 'while' is evaluated after the body has already run, so it cannot make get() safe. Move the check in front of the body as a pre-flow guard on the 'do'. See ek9 -h E08030 for details.

Incorrect:

      preFlowName <- lookupName()
      do
        stdout.println(`Pre-flow guard: ${preFlowName.get()}`)

Correct:

      do preFlowName <- lookupName()
        stdout.println(`Pre-flow guard: ${preFlowName.get()}`)

E08030 — Safe access is only inferred from a simple is-set check, or several joined with 'and'. Putting the is-set check under 'or' (or under 'not') makes the expression one the analysis will not reason about, so the body is not marked safe. Keep the is-set check as a plain 'and' operand. See ek9 -h E08030 for details.

Incorrect:

while leadingName? or stillGoing

Correct:

while leadingName? and stillGoing

E08040 — Inside a scope that a check has made safe, the guarded variable cannot be reassigned - that would invalidate the guarantee the check established. End the loop with a separate flag instead. See ek9 -h E08040 for details.

Incorrect:

        stdout.println(`Leading while: ${leadingName.get()}`)
        leadingName: lookupName()
        stillGoing: false

Correct:

        stdout.println(`Leading while: ${leadingName.get()}`)
        stillGoing: false

Coming from another language?

Java: Optional has no loop integration; you call isPresent() then get(), and a do-while gives no help either way - the compiler never checks. Kotlin: smart casts do not survive into a do-while body from the trailing condition, and null-safety is enforced by the type system rather than by flow position, so you use '?.let' or '!!'. Swift: 'repeat { } while' cannot bind an optional; 'guard let' before the loop is the idiom, which is closest to EK9's outer-if form. Rust: 'loop { }' with 'if let Some(v) = opt' inside re-matches every iteration; there is no trailing-condition binding. Go: no Optional; a nil check before the loop, unverified by the compiler. C#: nullable reference analysis does flow-sensitive checks but treats a do-while trailing condition as not guarding the body, the same conclusion EK9 reaches - though C# emits a warning where EK9 emits an error. EK9: the check must be positioned before the access, and the compiler proves it; a pre-flow guard on 'do' is the construct that puts a check before a post-condition loop body.

Keywords: condition, do, access, E08030, safe, postcondition, E08040, iterator, while, loop, optional, guard, trailing, preflow, result, get, unwrap