Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
An example is of course not a proof. But formal (e.g. machine-checkable) proofs of program correctness are not for the faint of heart. Are you sure that's what you want, rather than just an informal argument that will convince you and/or a human reader that the algorithm achieves what you want it to? –  Henning Makholm Nov 22 '11 at 23:05
(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). –  Henning Makholm Nov 22 '11 at 23:14

1 Answer 1

up vote 1 down vote accepted

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.

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.