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.