Loop invariant

A statement true whenever execution reaches a chosen point in a loop, usually immediately before its condition is tested. Establish it initially, preserve it through each iteration, and combine it with the exit condition to establish algorithm correctness. Termination needs a separate argument.^[ref]

Write

I

for the loop invariant,

B

for the condition,

P

for the precondition, and

Q

for the postcondition. Prove that initialization under

P

establishes

I

, that a completed body starting with

I

and

B

restores

I

, and that

I

with false

B

implies

Q

.^[ref]

In the prefix maximum correctness example, the loop invariant remembers exactly the maximum of the processed prefix and the valid index bounds. The weaker statement

best \geq a_{0}

survives every iteration, but does not imply the postcondition: for

[3, 1, 4, 4, 2]

, the wrong value

3

satisfies it. A useful loop invariant retains enough information to recover the answer when the condition becomes false.

Table of contents
- Loop variant Loop invariant

Loop variant ( $V$ )

 1  0

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

V = n - k

. It counts unread entries and is independent of whether the new entry changes the maximum. Ties therefore cannot stall progress:

k

increases even when

best

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

1, 1/2, 1/4, \dots

strictly decreases and is bounded below by zero, but never reaches zero. Choosing an integer measure avoids this failure.

 View more

A **loop invariant** is a property or condition that holds true before and after each iteration of a loop in a computer program. It is used primarily in the context of program correctness and formal verification to help understand and prove that a loop behaves as intended. The concept of a loop invariant is important in analyzing loops for correctness, particularly when applying proofs by induction.

 Read the full article

  See all articles in the same topic Create my own version

Loop invariant

Loop variant ( $V$ )

 Ancestors (4)

 Incoming links (221)

 Discussion (0) New discussion

 Articles by others on the same topic (1)

Loop invariant

Loop variant (V)

 Ancestors (4)

 Incoming links (221)

 Discussion (0)  Subscribe (1) New discussion

 Articles by others on the same topic (1)

Loop variant ( $V$ )

 Discussion (0) New discussion