Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

Two Programs for \bf SCM. Part II - Programs


Grzegorz Bancerek
Polish Academy of Sciences, Institute of Mathematics, Warsaw
Piotr Rudnicki
University of Alberta, Department of Computing Science, Edmonton

Summary.

We prove the correctness of two short programs for the {\bf SCM} machine: one computes Fibonacci numbers and the other computes the {\em fusc} function of Dijkstra [5]. The formal definitions of these functions can be found in [4]. We prove the total correctness of the programs in two ways: by conducting inductions on computations and inductions on input data. In addition we characterize the concrete complexity of the programs as defined in [3].

This work was partially supported by NSERC Grant OGP9207 while the first author visited University of Alberta, May--June 1993.

MML Identifier: FIB_FUSC

The terminology and notation used in this paper have been introduced in the following articles [9] [1] [7] [2] [6] [3] [8] [4]

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural 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 Piotr Rudnicki. Development of terminology for \bf scm. Journal of Formalized Mathematics, 5, 1993.
[4] Grzegorz Bancerek and Piotr Rudnicki. Two programs for \bf scm. Part I - preliminaries. Journal of Formalized Mathematics, 5, 1993.
[5] Edsger W. Dijkstra. \em Selected Writings on Computing, a Personal Perspective.
[6] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.
[7] Konrad Raczkowski and Andrzej Nedzusiak. Real exponents and logarithms. Journal of Formalized Mathematics, 2, 1990.
[8] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Journal of Formalized Mathematics, 5, 1993.
[9] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

Received October 8, 1993


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