@MISC{SCMISORT.MIZ,
  AUTHOR = {Chen, Jing-Chao},
  TITLE = {Insert Sort on {\SCMFSA}},
  NOTE = {This research is supported by the National Natural Science
       Foundation of China Grant No. 69873033.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Basic Property of {\bf while} Macro},
  SECTION3 = {Insert Sort Algorithm},
  DAY = {13},
  MONTH = {March},
  YEAR = {1999},
  ADDRESS1 = {Shanghai Jiaotong University},
  SUMMARY = {This article describes the insert sorting algorithm
  using macro instructions such as if-Macro (conditional
  branch  macro instructions), for-loop macro instructions
  and While-Macro instructions etc. From the viewpoint of
  initialization, we generalize the halting and computing
  problem of the While-Macro. Generally speaking, it is difficult
  to judge whether the While-Macro is halting or not by way of
  loop inspection. For this reason, we introduce a practical and
  simple method, called body-inspection. That is, in many cases,
  we can prove the halting problem of the While-Macro by only
  verifying the nature of the body of the While-Macro, rather than
  the While-Macro itself. In fact, we have used this method in justifying
  the halting  of the insert sorting algorithm. Finally, we prove that
  the insert  sorting algorithm given in the article is autonomic
  and its computing result is correct.}}

