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, MayJune 1993.
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]