Loop invariant of Selection Sort

algorithm-analysisalgorithms

 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 ?

Best Answer

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.

Related Topic