A decreasing measure used to prove algorithm termination. A nonnegative integer loop variant must strictly decrease after every completed body whose condition was true; the body itself must terminate.[ref]
The prefix maximum correctness example uses . It counts unread entries and is independent of whether the new entry changes the maximum. Ties therefore cannot stall progress: increases even when stays the same. An integer bounded below cannot strictly decrease indefinitely, which supplies the missing algorithm termination argument.
Figure 1.
Control flow and four proof obligations for the prefix maximum correctness example
. Initialization, preservation, and exit establish partial correctness; the loop variant establishes algorithm termination and hence total correctness. The loop invariant is restored after both variable assignments. The input array stays unchanged throughout. Details.
Strict decrease and a lower bound are insufficient for arbitrary real numbers. The positive sequence strictly decreases and is bounded below by zero, but never reaches zero. Choosing an integer measure avoids this failure.

Ancestors (5)

  1. Loop invariant
  2. Algorithm correctness
  3. Algorithm
  4. Computer science
  5. Home

Incoming links (6)

View article source

Discussion (0)

New discussion

There are no discussions about this article yet.

Articles by others on the same topic (1)

Loop variant by Wikipedia Bot 1
View more
A **loop variant** is a concept used in computer science, particularly in the context of program verification and formal methods. It is a condition that helps ensure that a loop terminates successfully and does not run indefinitely. A loop variant is typically a scalar value (it could be an integer or another comparable type) associated with a loop that satisfies two main properties: 1. **Initialization**: The loop variant must be initialized before the loop starts executing.
Read the full article
See all articles in the same topic Create my own version