<p>A very detailed proof you can find in online Stanford course by Tim Roughgarden here: <a href="https://class.coursera.org/algo/lecture/preview" rel="nofollow">https://class.coursera.org/algo/lecture/preview</a>
If you want slides you should sign in.</p>

CC BY-SA 3.0
2012-07-03T10:05:34.543Z
2012-07-03T10:05:34.543Z
avsmal
<p>Tobias Nipkow has formalised a proof in Isabelle/HOL, have a look <a href="http://isabelle.in.tum.de/library/HOL/ex/Quicksort.html" rel="nofollow">here</a>  (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 href="http://www.sussex.ac.uk/Users/mfb21/publications/icfp05/index.html" rel="nofollow">A Logical Analysis of Aliasing in Imperative Higher-Order Functions</a> 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.</p>

CC BY-SA 3.0
2012-07-03T14:17:45.470Z
2012-07-03T14:17:45.470Z
Martin Berger
<p>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. </p>

<p>a typical implementation of in-place Quick sort like this</p>

<pre><code>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 &lt;= 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] &lt; 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] &gt; 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 &lt;= j) {
            exchange(i, j);
            i++;
            j--;
        }
    }
    // Recursion
    if (low &lt; j)
        quicksort(low, j);
    if (i &lt; high)
        quicksort(i, high);
}

private void exchange(int i, int j) {
    int temp = numbers[i];
    numbers[i] = numbers[j];
    numbers[j] = temp;
}}
</code></pre>

<p>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.</p>

<p><strong>I think my question is actually to proof of correctness of partition method used in in-place Quicksort</strong></p>

CC BY-SA 3.0
2012-07-03T10:23:04.620Z
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
CC BY-SA 3.0
2012-07-03T11:24:39.623Z
@VittorioPatriarca yes, I mean proof of correctness
didxga
CC BY-SA 3.0
2012-07-03T14:10:32.717Z
@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
CC BY-SA 3.0
2012-07-03T15:00:45.257Z
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
CC BY-SA 3.0
2012-07-03T15:01:57.517Z
Please consider posting general level CS questions on [cs.se].
Kaveh
CC BY-SA 3.0
2012-07-03T17:12:24.553Z
@MartinBerger I don't completely understand your comment on my comment. Probably, it is simply a misunderstanding, since I'm not an english native speaker. Anyway, I was only pointed out that an algorithm is an object; you don't prove it. You prove that an algorithm is valid or that has a particular characteristic. Obviously, you need to formalize the algorithm before to prove something about it. A Java implementation is far from being a good description of an algorithm.
Vittorio Patriarca
<ds.algorithms><sorting>
Proof of correctness of in-place Quick sort
didxga
# Proof of correctness of in-place Quick sort

(Asked by: username_0 on 2012-07-03)

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

**Tags:** ds.algorithms, sorting
> **Comments:**
> **username_1**: Your question is probably more suited for CS. Anyway an algorithm is not a theorem, do you want to prove that it works?  
> **username_0**: @VittorioPatriarca yes, I mean proof of correctness  
> **username_2**: @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).  
> **username_3**: 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.  
> **username_3**: Please consider posting general level CS questions on [cs.se].  
> **username_1**: @MartinBerger I don't completely understand your comment on my comment. Probably, it is simply a misunderstanding, since I'm not an english native speaker. Anyway, I was only pointed out that an algorithm is an object; you don't prove it. You prove that an algorithm is valid or that has a particular characteristic. Obviously, you need to formalize the algorithm before to prove something about it. A Java implementation is far from being a good description of an algorithm.  

---

## 2 answers

### Answer by username_4 on 2012-07-03. Score: 3

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.


---

### Answer by username_2 on 2012-07-03. Score: 0

Tobias Nipkow has formalised a proof in Isabelle/HOL, have a look [here](http://isabelle.in.tum.de/library/HOL/ex/Quicksort.html) (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](http://www.sussex.ac.uk/Users/mfb21/publications/icfp05/index.html) 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.


---

