Loop Invariant

Definition

  • An invariant is a statement about program variables that is consistently true each time the program's execution reaches the invariant.

  • A loop invariant is a statement about program variables that remains true before and after each iteration of a loop. This serves to demonstrate that the result stays consistent with each iteration of the program loop.

Condition

A loop invariant is a key property used in validating the correctness of an algorithm. There are three essential conditions that must be met to affirm a loop invariant:

  1. Initialization: The loop invariant must hold true prior to the first execution of the loop.

  2. Maintenance: If the invariant holds true before an iteration of the loop, it should still hold true after the iteration.

  3. Termination: When the loop terminates, the invariant should provide us with meaningful information that helps us understand the algorithm.

How to use

  1. We show that the loop rule holds true before the loop starts.

  2. We assume this rule still holds at the beginning of a certain round of the loop (let's call it the jthj^{th}round).

  3. We prove that this rule remains true at the start of the following round (the (j+1)th(j+1)^{th} round).

  4. We describe what happens when the loop finishes and confirm that we get a useful result.

Example - Insertion Sort

Loop Invariant: Prior to the start of the jth loop, A[1..j-1] is sorted.

INSERTON-SORT(A)
for j = 2 to A.length
    key = A[j]
    i = j - 1
    while i > 0 and A[i] > key
	A[i+1] = A[i] // move the elements until it finds the location of the key
	i = i-1
    A[i+1] = key

Initial Condition: When j=2, the array A[1..1] only contains one value and is sorted.

Maintenance Condition: Assume that prior to the start of the jth iteration of the loop, A[1..j-1] is sorted. The while loop in our program moves the array to the right until it finds the correct position for sorting the key. After inserting the key into its correct position and incrementing j by 1, A[1..j] is sorted, preserving the loop invariant for the start of the j+1 iteration.

Termination Condition: When j=A.length+1, i=A.length, the loop terminates, and A[1..A.length] is sorted.

Therefore, the loop invariant is maintained, and the algorithm is valid.

More to read:

Last updated