Justifying the Correctness of the Fibonacci Sequence and the Euclide Algorithm by Loop-Invariant

Jing-Chao Chen

Shanghai Jiaotong University

Summary.

If a loop-invariant exists in a loop program, computing its result by loop-invariant is simpler and easier than computing its result by the inductive method. For this purpose, the article describes the premise and the final computation result of the program such as ``while$<$0'', ``while$>$0'', ``while$<>$0'' by loop-invariant. To test the effectiveness of the computation method given in this article, by using loop-invariant of the loop programs mentioned above, we justify the correctness of the following three examples: Summing $n$ integers (used for testing ``while$>$0''), Fibonacci sequence (used for testing ``while$<$0''), Greatest Common Divisor, i.e. Euclide algorithm (used for testing ``while$<>$0'').

This research is partially supported by the National Natural Science Foundation of China Grant No. 69873033.

MML Identifier: SCPINVAR

Contents (PDF format)

1. Preliminaries
2. Computing Directly the Result of ``while$<$0'' Program by Loop-Invariant
3. An Example: Summing Directly $n$ Integers by Loop-Invariant
4. Computing Directly the Result of ``while$>$0'' Program by Loop-Invariant
5. An Example: Computing Directly Fibonacci Sequence by Loop-Invariant
6. The Construction of ``while$<>$0'' Loop Program
7. The Basic Property of ``while$<>$0'' Program
8. Computing Directly the Result of ``while$<>$0'' Program by Loop-Invariant
9. An Example: Computing Greatest Common Divisor (Euclide Algorithm) by Loop-Invariant

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.

[4] Grzegorz Bancerek. Joining of decorated trees. Journal of Formalized Mathematics, 5, 1993.

[5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[6] Grzegorz Bancerek and Piotr Rudnicki. Two programs for \bf scm. Part I - preliminaries. Journal of Formalized Mathematics, 5, 1993.

[7] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

[8] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[9] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[10] 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.

[11] Jing-Chao Chen. Computation and program shift in the SCMPDS computer. Journal of Formalized Mathematics, 11, 1999.

[12] Jing-Chao Chen. Computation of two consecutive program blocks for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[13] Jing-Chao Chen. The construction and computation of conditional statements for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[14] Jing-Chao Chen. The construction and shiftability of program blocks for SCMPDS. Journal of Formalized Mathematics, 11, 1999.

[15] Jing-Chao Chen. Recursive Euclide algorithm. Journal of Formalized Mathematics, 11, 1999.

[16] Jing-Chao Chen. The SCMPDS computer and the basic semantics of its instructions. Journal of Formalized Mathematics, 11, 1999.

[17] Jing-Chao Chen. The construction and computation of while-loop programs for SCMPDS. Journal of Formalized Mathematics, 12, 2000.

[18] Jing-Chao Chen. Insert sort on SCMPDS. Journal of Formalized Mathematics, 12, 2000.

[19] Andrzej Kondracki. The Chinese Remainder Theorem. Journal of Formalized Mathematics, 9, 1997.

[20] Rafal Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Journal of Formalized Mathematics, 2, 1990.

[21] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.

[22] Yatsuka Nakamura and Andrzej Trybulec. On a mathematical model of programs. Journal of Formalized Mathematics, 4, 1992.

[23] Yasushi Tanaka. On the decomposition of the states of SCM. Journal of Formalized Mathematics, 5, 1993.

[24] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[25] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

[26] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Journal of Formalized Mathematics, 5, 1993.

[27] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[28] Wojciech A. Trybulec. Groups. Journal of Formalized Mathematics, 2, 1990.

[29] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[30] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.