Correctness of Non Overwriting Programs. Part I

Abstract

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 restrictions for the non overwriting program. For statements, only the following are allowed: “substituting-statement”, “f-else-statement”, “for-statement” (with break and without break), function (correct one) -- “call-statement” and “return-statement”. Grammar of non overwriting program is like the one of the C-language. For type of variables, “int”, “real", “char” and “float” can be used, 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.\par 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 {\it function-wise}. We must use only {\it correctness-proven} functions to define a new function (to write a new program as a form of a function). Here, we present two programs 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 perform an area check of the index of arrays used in one of the programs.