Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

Memory Handling for \SCMFSA


Piotr Rudnicki
University of Alberta, Edmonton
Andrzej Trybulec
Warsaw University, Bialystok

Summary.

We introduce some terminology for reasoning about memory used in programs in general and in macro instructions (introduced in [23]) in particular. The usage of integer locations and of finite sequence locations by a program is treated separately. We define some functors for selecting memory locations needed for local (temporary) variables in macro instructions. Some semantic properties of the introduced notions are given in terms of executions of macro instructions.

This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

MML Identifier: SF_MASTR

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

Contents (PDF format)

  1. Preliminaries
  2. Uniqueness of instruction components
  3. Integer locations used in macros
  4. Finite sequence locations used in macros
  5. Choosing an integer location not used in a program
  6. Choosing a finite sequence location not used in a program
  7. Semantics

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.
[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.
[8] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. 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] Agata Darmochwal and Andrzej Trybulec. Similarity of formulae. Journal of Formalized Mathematics, 3, 1991.
[12] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.
[13] Andrzej Nedzusiak. $\sigma$-fields and probability. Journal of Formalized Mathematics, 1, 1989.
[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. Semilattice operations on finite subsets. Journal of Formalized Mathematics, 1, 1989.
[17] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[18] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[19] Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 1989.
[20] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Journal of Formalized Mathematics, 5, 1993.
[21] Andrzej Trybulec and Yatsuka Nakamura. Modifying addresses of instructions of \SCMFSA. Journal of Formalized Mathematics, 8, 1996.
[22] Andrzej Trybulec and Yatsuka Nakamura. Relocability for \SCMFSA. Journal of Formalized Mathematics, 8, 1996.
[23] Andrzej Trybulec, Yatsuka Nakamura, and Noriko Asamoto. On the compositions of macro instructions. Part I. Journal of Formalized Mathematics, 8, 1996.
[24] Andrzej Trybulec, Yatsuka Nakamura, and Piotr Rudnicki. The \SCMFSA computer. Journal of Formalized Mathematics, 8, 1996.
[25] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[26] Wojciech A. Trybulec. Groups. Journal of Formalized Mathematics, 2, 1990.
[27] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[28] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received July 18, 1996

[ Download a postscript version, MML identifier index, Mizar home page]