@MISC{PRGCOR_2.MIZ,
  AUTHOR = {Nishiyama, Takaya and Fukura, Hirofumi and Nakamura, Yatsuka},
  TITLE = {Logical Correctness of Vector Calculation Programs},
  DAY = {13},
  MONTH = {July},
  YEAR = {2004},
  ADDRESS1 = {Shinshu University\\Nagano},
  ADDRESS2 = {Shinshu University\\Nagano},
  ADDRESS3 = {Shinshu University\\Nagano},
  SUMMARY = {In C-program, vectors of $n$-dimension are sometimes represented by arrays, where the dimension n is saved in the 0-th element of each array. If we write the program in non-overwriting type, we can gi
   Here, we give a program calculating inner product of 2 vectors, as an example of such a type, and its Logical-Model.
   If the Logical-Model is well defined, and theorems tying the model with    previous definitions are given, we can say that the program is correct logically.
   In case the program is given as implicit function form (i.e., the result of calculation is given by a variable of one of arguments of a function), its Logical-Model is given by a definition of a ne
   Logical correctness of such a program is shown by theorems following the definition.
   As examples of such programs, we presented vector calculation of add, sub, minus and scalar product.}}

