@MISC{SCMBSORT.MIZ,
  AUTHOR = {Chen, Jing-Chao and Nakamura, Yatsuka},
  TITLE = {Bubble Sort on {\SCMFSA}},
  DAY = {17},
  MONTH = {June},
  YEAR = {1998},
  ADDRESS1 = {Shanghai Jiaotong University},
  ADDRESS2 = {Shinshu University\\Nagano},
  SUMMARY = {We present the bubble sorting algorithm using macro instructions
  such as the if-Macro (conditional branch macro instructions) and
  the Times-Macro (for-loop macro instructions) etc. The correctness proof
  of the program should include the proof of autonomic, halting and the
  correctness of the program result. In the three terms, we justify
  rigorously the correctness of the bubble sorting algorithm. In order
  to prove it is autonomic, we use the following theorem: if all variables used
  by the program are initialized, it is autonomic. This justification
  method probably reveals that autonomic concept is not important.}}

