1
$\begingroup$

I'm new to this forum so please be patient.

I'm studying two sort algorithms: counting sort and bucket sort.

In numerous books I found examples, as a 'proof' that these algorithms work, but those test use a specific set of values.

So I want to know how can I do a formal mathematical proof of the working of the mentioned algorithms.

Any clue will help, I don't know exactly where to start(of course if you can provide a method would be better)

Thanks in advance

  • 0
    (The idea of formal proofs of programs has been around for about as long as there has been programs, but it has never been made non-cumbersome enough to see any _general_ use on real code. There are techniques for proving that a program doesn't do anything horribly _wrong_ (such as dereferencing null pointers), but proving that you get the _right result_ is something entirely different. We can manage simple and modular cases such as sorting algorithms, but the goal of producing proofs that entire software systems satisfy a formal specification document has remained a pipe dream).2011-11-22

1 Answers 1

1

In general, without making any reference to the two particular algorithms mentioned, there are (at least) two ways of proving the correctness of a sorting algorithm:

  • Proof by induction: assume that the algorithm can correctly sort $n$ items, and show that it can then also sort $n+1$ (or $2n$ or any other number greater than $n$) items. This works particularly well for recursive sorting algorithms like quicksort or merge sort.

  • Proof by termination analysis: show that the algorithm must terminate, and that it can only terminate when the data is correctly sorted. One way to show that the algorithm must terminate is to find a property (such as the number of inversions) which is bounded from below and can be shown to decrease by at least one during each iteration of the algorithm.