# 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'[0]\leq A'[1] \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


Clearly your conditions are lacking.

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'[0] \leq \dots \leq A'[n-1]$.

(3) The multisets $\{A[0],\ldots,A[n-1]\}$ and $\{A'[0],\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. –  Trinarics Feb 21 at 13:49
This is a program satisfying the two conditions you mentioned, termination and $A'[0] \leq A'[1] \leq \dots \leq A'[n]$. These conditions don't imply that the given procedure sorts its input. –  Yuval Filmus Feb 21 at 13:50
I said 'sorts'. How did that change to 'terminates'? –  Trinarics Feb 21 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 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'[0] \leq \dots \leq A'[N-1]$. –  Yuval Filmus Feb 21 at 14:23

To prove that bubble-sort works, you have to prove that:

1. It outputs after finite time.
2. The output is the (input) array sorted (each element is greater or equal than its previous, and each and only the elements of the input array appear in the output).

To prove that the algorithm always stop is easy (finite number of operations). I would prove the correctness of bubble sort by proving that on each iteration we add at least one element to its correct place, and that from this moment, the element will stay in this place. You have n-1 iterations, so after them n-1 elements are in their indexes and so is the last element.

-
Your answers falls into the same pitfall I mention in my answer: it's not enough to demand that the output array is sorted, since this can be satisfied trivially by outputting some fixed sorted array. –  Yuval Filmus Feb 21 at 14:07
@YuvalFilmus I wrote "the array". I didn't write "an array" or "some array". Anyway, I will try to further clarify my answer. –  Gari BN Feb 21 at 14:11
Imagine we didn't know what a sorting procedure did - how could we then understand what the phrase "the input array sorted"? –  Yuval Filmus Feb 21 at 14:18