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.

StackExchange Computer Science Q#21883, answer score: 9