# Proof of correctness of in-place Quick sort

I have found proof of correctness of Quick sort (not in-place version), Please refer me a proof of correctness of in-place Quick sort, or provide proof here is very appropriated.

a typical implementation of in-place Quick sort like this

public class Quicksort  {
private int[] numbers;
private int number;

public void sort(int[] values) {
// Check for empty or null array
if (values ==null || values.length==0){
return;
}
this.numbers = values;
number = values.length;
quicksort(0, number - 1);
}

private void quicksort(int low, int high) {
int i = low, j = high;
// Get the pivot element from the middle of the list
int pivot = numbers[low + (high-low)/2];

// Divide into two lists
while (i <= j) {
// If the current value from the left list is smaller then the pivot
// element then get the next element from the left list
while (numbers[i] < pivot) {
i++;
}
// If the current value from the right list is larger then the pivot
// element then get the next element from the right list
while (numbers[j] > pivot) {
j--;
}

// If we have found a values in the left list which is larger then
// the pivot element and if we have found a value in the right list
// which is smaller then the pivot element then we exchange the
// values.
// As we are done we can increase i and j
if (i <= j) {
exchange(i, j);
i++;
j--;
}
}
// Recursion
if (low < j)
quicksort(low, j);
if (i < high)
quicksort(i, high);
}

private void exchange(int i, int j) {
int temp = numbers[i];
numbers[i] = numbers[j];
numbers[j] = temp;
}}


the "pointer" i, j has different move track for different data, there are many case to consider here to proof that the i and j are pointed just in the right index after each recursion that all elements with index less than j is less than or equal to pivot, and all elements with index great than i is great than or equal to pivot.

I think my question is actually to proof of correctness of partition method used in in-place Quicksort

• Your question is probably more suited for CS. Anyway an algorithm is not a theorem, do you want to prove that it works? – Vittorio Patriarca Jul 3 '12 at 10:23
• @VittorioPatriarca yes, I mean proof of correctness – didxga Jul 3 '12 at 11:24
• @VittorioPatriarca Properly verifying Quicksort at a level of detail that a mathemtical journal would accept, let alone an interactive theorem prover (i.e. going beyond handwaving) isn't all that trivial, especially when talking about polymorphic quicksort. The main issue is not the proof as such, but setting up the formal framework to do the proof (e.g. think about what happens when a polymorphic comparison function has side-effects). – Martin Berger Jul 3 '12 at 14:10
• Welcome to cstheory, a Q&A site for research-level questions in theoretical computer science (TCS). Your question does not appear to be a research-level question in TCS. Please see the FAQ for more information on what is meant by this and suggestions for sites that might welcome your question. Finally, if your question is closed for being out of scope, and you believe you can edit the question to make it a research-level question, please feel free to do so. Closing is not permanent and questions can be reopened, check the FAQ for more information. – Kaveh Jul 3 '12 at 15:00
• Please consider posting general level CS questions on Computer Science. – Kaveh Jul 3 '12 at 15:01

A very detailed proof you can find in online Stanford course by Tim Roughgarden here: https://class.coursera.org/algo/lecture/preview If you want slides you should sign in.

Tobias Nipkow has formalised a proof in Isabelle/HOL, have a look here (I didn't check that this is the right proof, don't have time right now and I'm not super familiar with Isabelle/HOL, please feel free to edit if you find a better formalisation). The paper A Logical Analysis of Aliasing in Imperative Higher-Order Functions by N. Yoshida, K. Honda, and myself contains a sketch of a proof for polymorphic quicksort. The sketch assumes that the logic provides positive inductive definitions, which the logic we discuss in the rest of the paper doesn't (to keep the presentation simple). It's easy to add them.