# Formal Proof of Counting Sort and Bucket Sort Algorithms

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)

-
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

• 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.