@MISC{SCMPDS_7.MIZ,
  AUTHOR = {Chen, Jing-Chao and Rudnicki, Piotr},
  TITLE = {The Construction and Computation of for-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 of for-up loop Program},
  SECTION3 = {The Computation of for-up loop Program},
  SECTION4 = {The Construction of for-down loop Program},
  SECTION5 = {The Computation of for-down loop Program},
  SECTION6 = {Two Examples for Summing},
  DAY = {27},
  MONTH = {December},
  YEAR = {1999},
  ADDRESS1 = {Shanghai Jiaotong University},
  ADDRESS2 = {University of Alberta},
  SUMMARY = {This article defines two for-loop statements for SCMPDS. One is
  called for-up, which corresponds to ``for (i=x; i$<$0; i+=n) S''
  in C language.
  Another is called for-down, which corresponds to  
  ``for (i=x; i$>$0; i-=n) S''.
  Here, we do not present their unconditional halting (called parahalting)
  property, because we have not found that there exists a useful for-loop
  statement with unconditional halting, and the proof of
  unconditional halting is much simpler than that of conditional halting.
  It is hard to formalize all halting conditions, but some cases can be
  formalized. We choose loop invariants as halting conditions to prove
  halting problem of for-up/down statements. When some variables (except
  the loop control variable) keep undestroyed on a set for the loop
  invariant, and the loop body is halting for this condition,
  the corresponding for-up/down is halting and computable under this
  condition. The computation of for-loop statements can be realized
  by evaluating its body. At the end of the article, we verify
  for-down statements by two examples for summing.}}

