Loop Invariant - a property of a program loop that is true before (and after) each iteration

From: Wikipedia - Loop invariant

# EN

## Introduction to Algorithm

In the book Introduction to Algorithm, loop invariant is included in chapter 2.1, which is in the insertion sort. Loop invariant is employed to establish the correctness of the algorithm, which is also able to be applied on other algorithms.

Three conditions must to be held true:

**Initialization:**It is true prior to the first iteration of the loop**Maintenance:**If it is true before an iteration of the loop, it remains true before the next iteration.**Termination:**When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

In the case of insertion sorting, the ** loop invariant** is:

At the start of each iteration of the

forloop of line 1-8, the subarray consists of the elements originally in , but in sorted orders.

three conditions became:

**Initialization:**We start by showing that the loop invariant holds before the first loop iteration, when . The subarray , therefore, consists of just the single element , which is in fact the original element in . Moreover, this subarray is sorted (trivially, of course), which shows that the loop invariant holds prior to the first iteration of the loop.In plain word, this is saying, before the iteration starts, there is only one element in the sorted subarray, and therefore it’s sorted which satisfies the condition.

**Maintenance:**Next, we tackle the second property: showing that each iteration maintains the loop invariant. Informally, the body of the**for**loop works by moving , and so on by one position to the right until finds the proper position for , at which point it inserts the value of . The subarray then consists of the elements originally in , but in sorted order. Incrementing for the next iteration of the**for**loop then preserves the loop invariant.This is saying that, with each iteration, the values before current value are sorted.

**Termination:**Finally, we examine what happens when the loop terminates. The condition causing the**for**loop to terminate is that . Because each loop iteration increases by 1, we must have at that time. Substituting for in the wording of loop invariant, we have that the subarray consists of the elements originally in , but in sorted order. Observing that the subarray is the entire array, we conclude that the entire array is sorted. Hence, the algorithm is correct.When the loop ends, each element is iterated; the whole array is sorted. Consequently, the

**termination**determines the correctness of the algorithm.

## Other Explanation

I found that the example from wikipedia and What is a loop invariant? is very easy to understand.

### Wikipedia

1 | int max(int n,const int a[]) { |

### StackOverflow

1 | int j = 9; |

In this example it is true (for every iteration) that i + j == 9. A weaker invariant that is also true is that && .

# CN

## Introduction to Algorithm

# Reference

Introduction to Algorithm