@MISC{SCMPDS_8.MIZ,
  AUTHOR = {Chen, Jing-Chao},
  TITLE = {The Construction and Computation of While-Loop Programs for {SCMPDS}},
  NOTE = {This research is partially supported by the National Natural Science
       Foundation of China Grant No. 69873033.},
  SECTION1 = {Preliminaries},
  SECTION2 = {The Construction and Several Basic Properties of ``while$<$0'' Program},
  SECTION3 = {The Construction and Several Basic Properties of ``while$>$0'' Program},
  DAY = {14},
  MONTH = {June},
  YEAR = {2000},
  ADDRESS1 = {Shanghai Jiaotong University},
  SUMMARY = {This article defines two while-loop statements on SCMPDS, i.e.
  ``while$<$0'' and ``while$>$0'', which resemble the while-statements of
  the common high language such as C. We previously presented a
  number of tricks for computing while-loop statements on SCMFSA,
  e.g. step-while. However, after inspecting a few realistic examples,
  we found that they are neither very useful nor of generalization.
  To cover much more computation cases of while-loop statements,
  we generalize the computation model of while-loop statements,
  based on the principle of Hoare's axioms on the verification of
  programs.}}

