CODEWITHSUNDEEP
pythonproofcorrectness
KMAN
KMAN

Reputation: 39

Program correctness for a cubic sort program

I would like some help in proving my loop invariant for my python cubic sort program.

So far I figured out the loop invariant which has two parts

  1. 0 <= i+1 <= len(L)
  2. L[0:i+1] is sorted.
def cubicSort(L):
    i = 0
    while i + 1 < len(L):
        if L[i] > L[i + 1]:
            L[i], L[i + 1] = L[i + 1], L[i] # That is, swap L[i] and L[i + 1].
            i = 0
        else:
            i = i + 1

the precondition is L is a list of integers the post: is that the list is permuted and sorted

I don't know how to approach the proof

Upvotes: 0

Views: 134

Answers (1)

kaya3
kaya3

Reputation: 51093

There are two elements to a proof of correctness: you must prove that when the algorithm terminates, the result is correct; and you must prove that the algorithm does terminate.

Your two loop invariants are both right, but you do need to prove that they are invariants. To show this, you must show that they are true before the first iteration of the loop, and if they are true before some iteration then they will be true after that iteration.

After that's done, it's straightforward that when the loop terminates, i + 1 == len(L) and hence L[0:i+1] equals L, so it follows that L is sorted when the loop terminates.

Usually it is more straightforward to show that the algorithm terminates, by finding a loop variant - an integer quantity which gets smaller on each iteration of the loop, and which causes the loop to terminate when the quantity reaches 0. But for this algorithm, there is no obvious variant because the loop counter i is reset to 0 within the loop, meaning this variable doesn't simply keep getting bigger or smaller monotonically.

The key for this proof is to consider the number of inversions in the list, where an "inversion" means a pair of list elements which are out of order. On each iteration, either i gets bigger, or i is reset to 0 but the number of inversions is decreased by 1. It's not possible for i to keep getting bigger and for the number of inversions to keep getting smaller without either i reaching the while loop bound, or the number of inversions reaching 0. Once there are no inversions left in the list, L[i] > L[i + 1] is always false, so i will continue to increase up to the bound and then the loop terminates, as required.

Upvotes: 1

Related Questions