@MISC{SCPISORT.MIZ,
  AUTHOR = {Chen, Jing-Chao},
  TITLE = {Insert Sort on {SCMPDS}},
  NOTE = {This research is partially supported by the National Natural Science
       Foundation of China Grant No. 69873033.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Computing the Execution Result of For-Loop Program by Loop-Invariant},
  SECTION3 = {A Program for Insert Sort},
  SECTION4 = {The Property of Insert Sort and Its Correctness},
  DAY = {14},
  MONTH = {June},
  YEAR = {2000},
  ADDRESS1 = {Shanghai Jiaotong University},
  SUMMARY = {The goal of this article is to examine the effectiveness of ``for-loop''
  and ``while-loop'' statements on SCMPDS by insert sort. In this article,
  first of all, we present an approach to compute the execution result of
  ``for-loop'' program by ``loop-invariant'', based on Hoare's axioms for program
  verification. Secondly, we extend the fundamental properties of
  the finite sequence and complex instructions of SCMPDS. Finally, we prove
  the correctness of the insert sort program described in the article.}}

