Loop Correctness

Loop variants and invariants

NYI: There is currently no backend support to verify loop variants and invariants at runtime, so the example below would not fail even if the loop was not terminating or not satisfying the invariant...

Loops can be equipped with variants and invariants, which as expressions that help to verify that a loop terminates and produces the correct result.

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: The following loop example tries to find the first index of an array element that satisfy a condition is_what_we_want:

next: Loops and Tail Recursion