@MISC{PRGCOR_1.MIZ,
  AUTHOR = {Nakamura, Yatsuka},
  TITLE = {Correctness of Non Overwriting Programs. {P}art {I}},
  DAY = {05},
  MONTH = {December},
  YEAR = {2003},
  ADDRESS1 = {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 restrictions for the non overwriting program. For statements,
only the following are allowed: ``substituting-statement'', 
  ``if-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.}}

