Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

## The Construction and Computation of While-Loop Programs for SCMPDS

Jing-Chao Chen
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.

This research is partially supported by the National Natural Science Foundation of China Grant No. 69873033.

#### MML Identifier: SCMPDS_8

The terminology and notation used in this paper have been introduced in the following articles [22] [6] [19] [23] [5] [7] [14] [21] [2] [15] [16] [20] [17] [4] [13] [8] [1] [11] [9] [10] [12] [3] [18]

#### Contents (PDF format)

1. Preliminaries
2. The Construction and Several Basic Properties of ``while\$<\$0'' Program
3. The Construction and Several Basic Properties of ``while\$>\$0'' Program

#### Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.
[4] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.
[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[8] Jing-Chao Chen. Computation and program shift in the SCMPDS computer. Journal of Formalized Mathematics, 11, 1999.
[9] Jing-Chao Chen. Computation of two consecutive program blocks for SCMPDS. Journal of Formalized Mathematics, 11, 1999.
[10] Jing-Chao Chen. The construction and computation of conditional statements for SCMPDS. Journal of Formalized Mathematics, 11, 1999.
[11] Jing-Chao Chen. The construction and shiftability of program blocks for SCMPDS. Journal of Formalized Mathematics, 11, 1999.
[12] Jing-Chao Chen. Recursive Euclide algorithm. Journal of Formalized Mathematics, 11, 1999.
[13] Jing-Chao Chen. The SCMPDS computer and the basic semantics of its instructions. Journal of Formalized Mathematics, 11, 1999.
[14] Krzysztof Hryniewiecki. Recursive definitions. Journal of Formalized Mathematics, 1, 1989.
[15] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.
[16] Yatsuka Nakamura and Andrzej Trybulec. On a mathematical model of programs. Journal of Formalized Mathematics, 4, 1992.
[17] Yasushi Tanaka. On the decomposition of the states of SCM. Journal of Formalized Mathematics, 5, 1993.
[18] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[19] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[20] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Journal of Formalized Mathematics, 5, 1993.
[21] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[22] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[23] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.