Consider an
insertion sort. The outer loop counts
i through the array indexes. The inner loop finds the correct position for
a(
i) in the array, then inserts it.
The invariant is that indices 0 through i are sorted, and&that the array is a permutation of the original. Thus, when the termination condition is satisfied, the entire array is a sorted permutation of the original, which is what you wanted.