# Proving the Bubblesort actually sorts

Say $A'$ is the output of $\mathrm{Bubblesort}(A)$ on an array of length $N$. To prove that Bubblesort works, we have to prove that it always terminates and that $$A'\leq A' \leq \dots \leq A'[N-1].$$ Is there anything else that needs to be proven to show that Bubblesort actually sorts?

(I have found this question in a textbook about algorithms.)

Here is an algorithm which satisfies your conditions:

for i in 0,...,n-1:
A'[i] = 0


Correction of a sorting program, like any other program, is a combination of two condition: termination and partial correction. Termination just states that if the preconditions are satisfied then the program always terminates (in your course the phrase used is evidently "outputs after finite time", but halts or terminates is shorter). Partial correctness means that if the preconditions are satisfied and the program halts, then the postconditions are satisfied. What is left here is to come up with preconditions and postconditions. Since you're not working within a formal model, it is not clear how exactly to state the precondition, but it's probably something like that:

Precondition: The input $A$ is an array of length $N \geq 1$ of numbers.

(More generally, it is an array of some linearly ordered set, but we can think of "numbers" (whatever that means) as an important special case.)

Stating the postcondition is harder. It is not enough to ask that the output be sorted, as my example above shows. The semantics are subtler. Here is one way of stating the postcondition:

Postcondition: (1) The output array $A'$ is an array of length $N$ of numbers.

(2) The output array $A'$ is nondecreasing, i.e., $A' \leq \dots \leq A'[n-1]$.

(3) The multisets $\{A,\ldots,A[n-1]\}$ and $\{A',\ldots,A'[n-1]\}$ are equal, i.e., for each number $x$, the number of elements in $A$ equal to $x$ is the same as the number of elements in $A'$ equal to $x$.

The way that you prove postcondition (3) for bubble sort (and, more generally, for comparison sorts) is by showing that the swapping operation preserves the multiset of elements (the fast implementation of quicksort might need more care). So it might seem that you can replace (3) with the following postcondition:

(3') The array $A'$ is obtained from $A$ by a sequence of swaps.

There are two problems with this postcondition. First, it is not semantic — it doesn't describe what sorting accomplishes, only how sorting is done. Second, it is too restrictive. There are sorting algorithms which use operations beyond swapping. A particularly useful example is counting sort. Suppose the sorted numbers come from a very small domain, say $\{0,\dots,m-1\}$. We compute a histogram of the input array (using an integer array of length $m$), and then go over the histogram, producing a sorted version of the input.

• What? That's not what I ment. – HaloKiller Feb 21 '14 at 13:49
• This is a program satisfying the two conditions you mentioned, termination and $A' \leq A' \leq \dots \leq A'[n]$. These conditions don't imply that the given procedure sorts its input. – Yuval Filmus Feb 21 '14 at 13:50
• I said 'sorts'. How did that change to 'terminates'? – HaloKiller Feb 21 '14 at 13:51
• You need to explain what "sort" means. It doesn't mean that the output array is sorted. That's not enough. You have to relate the input array to the output array. – Yuval Filmus Feb 21 '14 at 14:09
• @FrankW I replaced "outputs after finite time" by terminates, and then "terminates" was mysteriously replaced by "sorts". I would say that the second hack is even worse than the first. The word "sorts" might have been there (can't remember) followed by the explanation $A' \leq \dots \leq A'[N-1]$. – Yuval Filmus Feb 21 '14 at 14:23

Apart from the given terminating condition the only condition required is to prove that A' contains all the elements of A , just that they have been permutated

• Thank you for your answer. However, it's not clear what it adds over Yuval Filmus's pre-existing answer. This requirement is already mentioned in his answer, and he shows how to formalize it more carefully. – D.W. Sep 1 '15 at 5:06
• I just described the answer in a simple manner. – Moharnab Saikia Sep 23 '15 at 23:06