# Loop invariant of Selection Sort

`````` Selection Sort(A[1,2..n]:array of integers)
1.for i=1  to n-1
2.for j=i+1 to n
3.if A[j]<A[i]
4     swap(A[i],A[j])
``````

I am trying to prove the correctness of this algorithm,I read from my book and here is what is written:We must have 2 invariants for the inner and outer loop

The inner states:Every time we reach line 2,the current A[i] hold the value of a minimum element from A[i ,...,j-1]

The outer states : Everytime we are at line 1,the current subarray A[1,..,i-1] consists of i-1 in number smallest elements from the original array A'[1,....,n] in sorted order

Now to prove that it is really sorting we use the outer loop with the claim that the part from A[1,..,i-1] is sorted and from the inner loop invariant A[i] is the minimum from A[1,...n] and it is solved ,however what seems unclear to me is how we design the inner invariant ,why do we say A[i] is the minimum from A[i,..,j-1] I tried with some values and it always turns only 1 element and I guess in our final proof we say not A[i] is the minimum in A[i,...j-1] but A[i,..n].Shouldn't we say A[i] is the minimum in A[i,..,j-1] since we have proved that ?

• If you are working from a book, perhaps you could tell us what book it is. – Mike Spivey Apr 25 '17 at 7:56

## 2 Answers

The analysis of the program would become easier if you rewrote the for loops as the equivalent while loops, because then it becomes obvious what is the value of the 'controlled variable' after the loop has finished. In this style, your inner loop is

``````j = i+1
(* Inv: i+1 <= j <= n+1 and A[i] = min A[i..j-1] *)
while j <= n:
if a[j] < a[i]:
swap(A[i], A[j])
j = j+1
``````

The invariant is true when j = i+1, and it is maintained by the loop body. When the loop terminates, we have j = n+1, and the invariant tells us that A[i] = min A[i..j-1] = min A[i..n]. That is what is needed to justify a claim that A[1..i] contains the smallest i elements of A in sorted order.

The outer loop becomes

``````i = 1
(* Inv: 1 <= i <= n and A[1..i-1] contains the smallest i-1
elements of A[1..n] in sorted order *)
while i <= n-1:
[Inner loop]
i = i+1
``````

So if the inner loop ends with A[1..i] as described, this turns into A[1..i-1] after taking into account the increment of i. The outer loop can terminate with i = n, because at that point we have selected and sorted n-1 elements of A, and the last remaining element must be the biggest.

It does no harm and aids clarity to make the ranges of variables like i and j explicit in the invariants.

Generally speaking: this sort of analysis becomes easier if you adopt 0-based indexing, because then the fog of +1's and -1's dissipates; but if your book uses 1-based indexing, I guess you're stuck with it. I also like to use the notation A[i..j) for A[i..j-1].

Some languages (dating back to Algol 60) say that the value of the controlled variable is undefined after a for loop, and others encourage us to make the variable local to the loop. Either way, we are discouraged from saying that its value after the loop is n+1, but that assertion is needed to make sense of what the invariant tells us about the state after the loop is finished. That's why I teach my students to mentally rewrite the loop as a while before analysis.

The proof is about sorting. To prove that an array is sorted, you just have to prove that there is the same order between all the successive numbers. Or otherwise stated, that every number in the array is at least as much as its predecessor.

Let's start ! The invariant of statement 3 (together with the `then` clause in 4) is that:

(I3): whatever the selected i and j, a[i] < a[j]

From this, we can infer the invariant of statement 2: the loop starts at i+1 and will loop until n, so it will ensure (I3) for all the numbers following i in the array.

(I2): whatever i, and whatever j between i+1 and n, a[i]< a[j]

From there, we move to invariant of statement 1: the loop starts at i=1 and will ensure that (I2) is true, so in particular that a1mathematical induction:

(I3): every number in the array is smaller than its successor

Or conversely, that:

every number in the array is greater or equal than the number before.

And this corresponds to the definition of a sorted array.

Using minimums can certainly be a way to go as well. But I'd take it only if I had a definition of a sorted array which would be based on minimums.