Correctness of Non Overwriting Programs. Part I

Yatsuka Nakamura

Shinshu University, Nagano

Summary.

Non overwriting program is a program where each variable used in it is written only just one time, but the control variables used for for-statement are exceptional. Contrarily, variables are allowed to be read many times. There are other restriction for non overwriting program. For statements, only the followings are allowed: substituting-statement, if-else-statement, for-statement(with break and without break), function(correct one)-call -statement and return-statement. Grammars of non overwriting program is like one of C-language. For type of variables, 'int','real","char" and "float" can be used, and and array of them can also be used. For operation, "+", "-" and "*" are used for a type int, "+","-","*" and "/" are used for a type float. User can also define structures like in C. Non overwriting program can be translated to (predicative) logic formula in definition part to define functions. If a new function is correctly defined, a corresponding program is correct, if it does not use arrays. If it uses arrays, area check is necessary in the following theorem. Semantic correctness is shown by some theorems following the definition. These theorems must tie up the result of the program and mathematical concepts introduced before. Correctness is proven function-wise. We must use only correctness-proven functions to define a new function(to write a new program as a form of a function). Here, we present two program of division function of two natural numbers and of two integers. An algorithm is checked for each case, by proving correctness of the definitions. We also do an area check of index of arrays used in one of the programs.

MML Identifier: PRGCOR_1

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] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[4] Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Euler's Theorem and small Fermat's Theorem. Journal of Formalized Mathematics, 10, 1998.

[5] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.

[6] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

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

[8] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.