Here is the general pattern of the use of Loop Invariants in your code:

... // the Loop Invariant must be true here while ( TEST CONDITION ) { // top of the loop ... // bottom of the loop // the Loop Invariant must be true here } // Termination + Loop Invariant = Goal ...Between the top and bottom of the loop, headway is presumably being made towards reaching the loop's goal. This might disturb (make false) the invariant. The point of Loop Invariants is the promise that the invariant will be restored before repeating the loop body each time.

There are two advantages to this:

- Work is not carried forward to the next pass in complicated, data dependent ways. Each pass through the loop in independent of all others, with the invariant serving to bind the passes together into a working whole.
- Reasoning that your loop works is reduced to reasoning that the loop invariant is restored with each pass through the loop. This breaks the complicated overall behavior of the loop into small simple steps, each which can be considered separately.

The test condition of the loop is not part of the invariant. It is what makes the loop terminate. You consider separately two things: why the loop should ever terminate, and why the loop achieves its goal when it terminates. The loop will terminate if each time through the loop you move closer to satisfying the termination condition. It is often easy to assure this: e.g. stepping a counter variable by one until it reaches a fixed upper limit. Sometimes the reasoning behind termination is more difficult.

The loop invariant should be created so that when the condition of termination is attained, and the invariant is true, then the goal is reached:

It takes practice to create invariants which are simple and relate which capture all of goal attainment except for termination. It is best to use mathematical symbols to express loop invariants, but when this leads to over-complicated situations, we rely on clear prose and common-sense.

Here is the general idea.
Let us call the array `A`, which has `n` elements in it.
We keep two variables, `nextToCheck` and `smallestSoFar`
We initially set `smallestSoFar` to 0, and compare `A[1],
A[2], ..., A[n-1]` against `A[smallestSoFar]`
If the current comparision shows a smaller value, we update
`smallestSoFar`.

Here is the Loop Invariant:

- smallestSoFar in [0,nextToCheck),
- and for all k in [0,nextToCheck), A[k] >= A[smallestSoFar].

We set the Loop Invariant true before the loop by setting:

nextToCheck = 1 ; smallestSoFar = 0 ;Each time through the loop we increment

if ( a[smallestSoFar] > a[nextToCheck] ) { smallestSoFar = nextToCheck ; } nextToCheck ++ ;The termination condition is

The combination of the loop invariant and the termination
condition gives that `smallestSoFar` is the
index of the smallest value in the array.

**Review:**

- Check that the Loop Invariant is
setup true by the initialization of
`nextToCheck`and`smallestSoFar`; - Check that each time through the loop, assuming the Loop Invariant true going into the loop, it is true going out of the loop;
- Check that headway towards termination is being made
(in this case,
`nextToCheck`is always incremented in the loop body). - Check that termination plus loop invariant equals goal attained.

A trick is used to move the selected integer from the front part of the array to the back part of the array. The selected integer is swapped with the integer in location i-1.

We make use of the function `FindMin( int A[], int n )`
which returns the index of the minimum value in array `A`
among array locations 0 through `n-1`. This function was
presented in the previous example.

The loop invariant is in terms of `numSorted`, the number of
elements already sorted from the array,

- The smallest
`numSorted`values are sorted in descending order in locations`[n-numSorted,n)`, - and the rest are in locations
`[0,n-numSorted)`.

numSorted=0 ;immidately makes the loop invariant true.

Each time through the loop increased `numSorted` by one.
To do this, the smallest from the front of the array needs to be
selected and swapped to the back of the array,

i = findMinumum(A,n-numSorted) ; numSorted++ ; swap( A, i, n-numSorted ) ;Terminate when

**Review:**

- Check that the Loop Invariant is
setup true by the initialization of
`numSorted`. - Check that each time through the loop, assuming the Loop Invariant true going into the loop, it is true going out of the loop;
- Check that headway towards termination is being made.
Here headway is obious:
`numSorted`is incremented each time through the loop. - Check that termination plus loop invariant equals goal attained.