:: Logical Correctness of Vector Calculation Programs :: by Takaya Nishiyama , Hirofumi Fukura and Yatsuka Nakamura :: :: Received July 13, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users
:: deftheorem Def2 defines IFLGTPRGCOR_2:def 2 : for x, y, a, b, c being set holds ( ( x in y implies IFLGT (x,y,a,b,c) = a ) & ( x = y implies IFLGT (x,y,a,b,c) = b ) & ( not x in y & not x = y implies IFLGT (x,y,a,b,c) = c ) );
:: Vector Calculation Program: Scalar Product of Vector
::
:: The following C program is correct if it is used under some limited
::conditions, which are shown in the theorem following the definition
::after this program.
:: But it still remains a possibility of overflow.
:: The following program does not take an explicit function form.
::It means the value of the function does not have a sense.
::The result of the calculation is
::given in a variable c. Precisely speaking, the result is not unique,
::because of the difference of initial value of c.
:: For a model of such a program, we propose the logical predicate form
::(we call such a model, Logical-Model of a program) in the following
::definition.
::
::#define V_SIZE 1024
::void scalar_prd_prg(float c[V_SIZE], float a, float b[V_SIZE])
::{ int n,i;
:: c[0]=b[0];
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=1;i<=n;i++)c[i]=a*b[i];
:: }
:: return;
::}
::The following definition is Logical-Model of the above program.
:: Vector Calculation Program: Sum of Vectors
::
:: The following program is the same type of scalar_prd_prg, but gives a result
:: a+b in a variable c.
::
::#define V_SIZE 1024
::void vector_add_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])
::{ int n,i;
:: c[0]=b[0];
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=1;i<=n;i++)c[i]=a[i]+b[i];
:: }
:: return;
::}
:: Vector Calculation Program: Subtraction of Vectors
::
:: The following program is the same type of scalar_prd_prg, but gives a result
:: a-b in a variable c.
::
::#define V_SIZE 1024
::void vector_sub_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])
::{ int n,i;
:: c[0]=b[0];
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=1;i<=n;i++)c[i]=a[i]-b[i];
:: }
:: return;
::}
::#define V_SIZE 1024
:: float inner_prd_prg(float a[V_SIZE],float b[V_SIZE]){
:: int n,i; float s[V_SIZE];
:: s[0]=0;
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=0;i<n;i++)s[i+1]=s[i]+a[i+1]*b[i+1];
:: }
:: return s[n];
:: }