@MISC{SCPQSORT.MIZ,
  AUTHOR = {Chen, Jing-Chao},
  TITLE = {Quick Sort on {SCMPDS}},
  NOTE = {This research is partially supported by the National Natural Science
       Foundation of China Grant No. 69873033.},
  SECTION1 = {The Several Properties of ``while'' Program and Finite Sequence},
  SECTION2 = {Program Partition is to Split a Sequence into a Smaller and
    a Larger Subsequence},
  SECTION3 = {The Construction of Quick Sort},
  SECTION4 = {The Basic Property of Partition Program},
  SECTION5 = {The Basic Property of Quick Sort and Its Correctness},
  DAY = {14},
  MONTH = {June},
  YEAR = {2000},
  ADDRESS1 = {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.}}

