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

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.