The SCMPDS Computer and the Basic Semantics of its Instructions

Jing-Chao Chen

Shanghai Jiaotong University

Summary.

The article defines the SCMPDS computer and its instructions. The SCMPDS computer consists of such instructions as conventional arithmetic, ``goto'', ``return'' and ``save instruction-counter'' (``saveIC'' for short). The address used in the ``goto'' instruction is an offset value rather than a pointer in the standard sense. Thus, we don't define halting instruction directly but define it by ``goto 0'' instruction. The ``saveIC'' and ``return'' equal almost call and return statements in the usual high programming language. Theoretically, the SCMPDS computer can implement all algorithms described by the usual high programming language including recursive routine. In addition, we describe the execution semantics and halting properties of each instruction.

This work was done while the author visited Shinshu University March--April 1999.

MML Identifier: SCMPDS_2

Contents (PDF format)

1. The SCMPDS Computer
2. The Memory Structure
3. The Instruction Structure
4. Execution Semantics of the SCMPDS instructions

Acknowledgments

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[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. A classical first order language. Journal of Formalized Mathematics, 2, 1990.

[8] 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.

[9] Jing-Chao Chen. A small computer model with push-down stack. Journal of Formalized Mathematics, 11, 1999.

[10] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[11] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.

[12] Yatsuka Nakamura and Andrzej Trybulec. On a mathematical model of programs. Journal of Formalized Mathematics, 4, 1992.

[13] Dariusz Surowik. Cyclic groups and some of their properties --- part I. Journal of Formalized Mathematics, 3, 1991.

[14] Yasushi Tanaka. On the decomposition of the states of SCM. Journal of Formalized Mathematics, 5, 1993.

[15] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.

[16] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[17] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[18] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[19] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Journal of Formalized Mathematics, 5, 1993.

[20] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[21] Wojciech A. Trybulec. Groups. 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.