Fuzion Logo
flang.dev — The Fuzion Language Portal
JavaScript seems to be disabled. Functionality is limited.

Loop Correctness

Loop variants and invariants

TBW!

loop variants and invariants are not implemented yet.

The idea is taken from Eiffel: A loop variant specifies a positive integer expression that provides an upper bound for the remaining loop iterations. This can be used for formal analysis to proof loop termination and it can be checked at run-time that this expression is strictly decreasing.

The loop invariant is a condition that holds before the first iteration of the loop body and remains true during the execution of one loop iteration. An example would be a loop to search a list for a specific element. Here the invariant might be that none of the elements before the current index matches the search.

For a successful loop, the invariant then ensures that the first found element is returned. For a failed loop, the invariant ensures that no element matches the search criterion.

Example:

  for
    i in 0..array.size-1
  variant
    array.size - i
  invariant
    (0..i-1) ∀ (fun (j i32) => !isWhatWeWant(array[i]))
  until isWhatWeWant(array[i])