Some Remarks on the Simple Concrete Model of Computer

Andrzej Trybulec

Warsaw University, Bialystok

Yatsuka Nakamura

Shinshu University, Nagano

Summary.

We prove some results on {\bf SCM} needed for the proof of the correctness of Euclid's algorithm. We introduce the following concepts: \begin{itemize} \item[-] starting finite partial state (Start-At$(l)$), then assigns to the instruction counter an instruction location (and consists only of this assignment), \item[-] programmed finite partial state, that consists of the instructions (to be more precise, a finite partial state with the domain consisting of instruction locations). \end{itemize} We define for a total state $s$ what it means that $s$ starts at $l$ (the value of the instruction counter in the state $s$ is $l$) and $s$ halts at $l$ (the halt instruction is assigned to $l$ in the state $s$). Similar notions are defined for finite partial states.

MML Identifier: AMI_3

Contents (PDF format)

1. A small concrete machine
2. Users guide
3. Preliminaries
4. Some Remarks on AMI-Struct
5. Instruction Locations and Data Locations
6. Halt Instruction

Bibliography

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

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

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

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

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

[6] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[7] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[8] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.

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

[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] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.

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

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

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

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

[19] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[20] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.