1. Loop invariants

Given that
 l < r: 
1. small < r  not an invariant: if all items in the partition range are
smaller than the pivot, after the last loop iteration small = r.

2. small < large: not an invariant for the same reason as above.

3. small <= large: this is an invariant: before the loop executed small <
large (because l < r) and after the last iteration, small = large.

4. for all i such that l <= i < small, arr[i] < pivot: this is a loop
invariant. Before the loop is executed, there are no such i. After each
iteration, items to the left of small are less than the pivot.

5. for all j such that large <= j <= r, arr[j] >= pivot: this is a loop
invariant. Before the loop is executed, large = r and the value at this
index is the pivot, so arr[j] = pivot. After each iteration, items at
the index large and to the right are greater or equal to the pivot.

6. for all j such that large < j <= r, arr[j] >= pivot: this is also
a loop invariant. It is a weaker statement than 5 so if 5 is true then 6
is true.

2. Correctness of selection sort

Algorithm

void  selectionSort(int arr[], int len){
   int i;
   int j;
   int temp;
   int pos_greatest;

   for( i = len - 1; i > 0; i--){
      pos_greatest = 0;
      for(j = 0; j <= i; j++){
         if( arr[j] > arr[pos_greatest]){
            pos_greatest =  j;
         }//end if
      }//end inner for loop
      temp = arr[i];
      arr[i] = arr[pos_greatest];
      arr[pos_greatest] = temp; 
   }//end outer for loop
}//end selection sort

Outline of the proof

We just formalise what we know the selection sort is doing, namely: at every passage through the inner loop, we find the largest element in the range [0,...,i]; the outer loop swaps that element to position i and decrements i. So the first passage through the outer loop swaps the largest element in the range [0,...,n-1] to position n-1, the next one swaps the largest element in the range [0,...,n-2] to position n-2 etc. There are many properties which stay invariant for the outer loop, and may be ours is not the most obvious choice, but let's say that the invariant of the outer loop is that the part of the array to the right of the loop counter is sorted in ascending order and that the numbers to the right are greater or equal to the numers remaining in the unsorted part. When we are finished this means that the whole array is sorted in ascending order.

Invariant of the inner loop

First we need to formulate precisely and prove the loop invariant of the inner loop: All numbers in the array up to and not including the position j are are less or equal to the number at pos_greatest (for all k < j, arr[k] <= arr[pos_greatest]).
Proof:

When the inner loop terminates, i < j. So the invariant of the inner loop implies that for all k <= i, arr[k] <= arr[pos_greatest], in other words, pos_greatest is the index of the greatest item between 0 and i (inclusive).

Invariant of the outer loop

Invariant: elements at positions strictly to the right of i to len-1 are sorted in ascending order and are greater than the elements to the left of i. More formally: for all k with i < k <= len-1, arr[k] <= arr[k+1]<=... <= arr[n-1] and for all m with 0 <= m <= i, arr[m] <= arr[k].

Proof that this property is an invariant of the outer loop:

And finally...

When i = 0 the invariant of the outer loop becomes
arr[0] <= arr[1] <= ... <= arr[len-1] so the array is sorted.