Nested Loops: the final lesson

So friday was the day where we were taught the last of chapter 2 (recurrences and correctness).  The topic was nested loops.  The idea of this proof is very similar to proofing a regular loop except we have to start from the inner loop first as that will determine if the outside loop can run its next execution in the loop.

Looking at the code that was provided on the overhead by Danny, the class assumed that the precondition will hold and that the code will terminate properly.  The for this assumption is the loops within the selection sort have the condition to terminate once the interger variable reaches the length of the array. This happens for both the inner loop and the outer loop.  But to convince a skeptic that this actually works we can prove that the length of the outer loop is transitively the upper bound of the length of the inner loop.

The method that selection sort works is it takes a look at each element (we call i) and compare each element starting from the (i + 1)th element all the way until the end of the array to see if there is an element with a value less than the i-th element and perform a swap.  This means that the distance between the (i+1)th element is always decreasing.  The Distance between i and the length of the array is also always decreasing.  This proves that both loops will terminate when i or i+1 is equal to the length of the array.  The code then returns the sorted array.

Thus the code is proven to meet its precondition which is to loop through the array and perform a selection sort and that it will terminate implying that the code is correct.