Quick Sort on SCMPDS

Jing-Chao Chen

Shanghai Jiaotong University / China Bell Labs

Summary.

Proving the correctness of quick sort is much more complicated than proving the correctness of the insert sort. Its difficulty is determined mainly by the following points: \begin{itemize} \item Quick sort needs to use a push-down stack. \item It contains three nested loops. \item A subroutine of this algorithm, ``Partition'', has no loop-invariant. \end{itemize} This means we cannot justify the correctness of the ``Partition'' subroutine by the Hoare's axiom on program verification. This article is organized as follows. First, we present several fundamental properties of ``while'' program and finite sequence. Second, we define the ``Partition'' subroutine on SCMPDS, the task of which is to split a sequence into a smaller and a larger subsequence. The definition of quick sort on SCMPDS follows. Finally, we describe the basic property of the ``Partition'' and quick sort, and prove their correctness.

This research is partially supported by the National Natural Science Foundation of China Grant No. 69873033.

MML Identifier: SCPQSORT

Contents (PDF format)

1. The Several Properties of ``while'' Program and Finite Sequence
2. Program Partition is to Split a Sequence into a Smaller and a Larger Subsequence
3. The Construction of Quick Sort
4. The Basic Property of Partition Program
5. The Basic Property of Quick Sort and Its Correctness

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[5] Grzegorz Bancerek and Piotr Rudnicki. Development of terminology for \bf scm. Journal of Formalized Mathematics, 5, 1993.

[6] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

[7] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[8] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[9] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[10] Jing-Chao Chen. Computation and program shift in the SCMPDS computer. Journal of Formalized Mathematics, 11, 1999.

[11] Jing-Chao Chen. Computation of two consecutive program blocks for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[12] Jing-Chao Chen. The construction and computation of conditional statements for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[13] Jing-Chao Chen. The construction and shiftability of program blocks for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[14] Jing-Chao Chen. Recursive Euclide algorithm. Journal of Formalized Mathematics, 11, 1999.

[15] Jing-Chao Chen. The SCMPDS computer and the basic semantics of its instructions. Journal of Formalized Mathematics, 11, 1999.

[16] Jing-Chao Chen. The construction and computation of while-loop programs for SCMPDS. Journal of Formalized Mathematics, 12, 2000.

[17] Jing-Chao Chen. Insert sort on SCMPDS. Journal of Formalized Mathematics, 12, 2000.

[18] Jaroslaw Kotowicz. Functions and finite sequences of real numbers. Journal of Formalized Mathematics, 5, 1993.

[19] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.

[20] Yatsuka Nakamura and Andrzej Trybulec. On a mathematical model of programs. Journal of Formalized Mathematics, 4, 1992.

[21] Piotr Rudnicki. The \tt for (going up) macro instruction. Journal of Formalized Mathematics, 10, 1998.

[22] Yasushi Tanaka. On the decomposition of the states of SCM. Journal of Formalized Mathematics, 5, 1993.

[23] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[24] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[25] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Journal of Formalized Mathematics, 5, 1993.

[26] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[27] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.