Vitte Loops

This page treats Vitte logic as an executable mechanism: each rule is linked to a concrete consequence in the program flow. A Vitte loop is correct when its state, progress, and exit are visible in the text without external inference.

proc sum_to(limit: int) -> int {
  let i: int = 0
  let acc: int = 0
  loop {
    if i > limit { break }
    set acc = acc + i
    set i = i + 1
  }
  give acc
}

Why this step is solid. Main invariant: before each output test, acc contains the sum of integers already scanned. The loop ends by explicit condition and monotonic mutation of i.

What happens at runtime. sum_to(3) produces the sequence acc=0,1,3,6 then returns 6.

proc sum_to_while(limit: int) -> int {
  let i: int = 0
  let acc: int = 0
  while i <= limit {
    set acc = acc + i
    set i = i + 1
  }
  give acc
}

Why this step is solid. while makes the continuation condition front-end without changing the Vitte execution model. This is the most direct writing when the invariant depends on a single Boolean test.

proc positive_sum(values: int[]) -> int {
  let acc: int = 0
  for x in values {
    if x < 0 { continue }
    set acc = acc + x
  }
  give acc
}

Why this step is solid. The for route relieves index management, continue removes values ​​outside the local contract. The state change remains unique.

What happens at runtime. [5,-3,4] leads to acc=0->5->5->9, exit 9.

proc find_first_positive(values: int[]) -> int {
  for x in values {
    if x > 0 { give x }
  }
  give 0
}

Why this step is solid. Early exit give in the loop. The first match closes the course; otherwise the function returns the neutral ending value.

What happens at runtime. [-2,-1,7,8] returns 7 to the third element. [-2,-1] returns 0.

This page extends book/chapters/07-control.html and refers to the keywords loop, for, break, continue in book/chapters/keywords/loop.html, book/chapters/keywords/for.html, book/chapters/keywords/break.html, book/chapters/keywords/continue.html.