:: Logical Correctness of Vector Calculation Programs
::  by Takaya Nishiyama , Hirofumi Fukura and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, XBOOLE_0, AFINSQ_1, SUBSET_1, TARSKI, CARD_1,
      FUNCT_1, RELAT_1, ORDINAL1, FINSEQ_1, XXREAL_0, ARYTM_3, ARYTM_1,
      FUNCOP_1, ORDINAL4, REAL_1, INT_1, CARD_3, PARTFUN1, RVSUM_1, FINSEQ_2,
      PRGCOR_2, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
      CARD_1, ORDINAL4, XREAL_0, REAL_1, VALUED_0, XCMPLX_0, NAT_1, PARTFUN1,
      FINSEQ_1, FUNCOP_1, AFINSQ_1, INT_1, RVSUM_1, NAT_D, FINSEQ_2, XXREAL_0;
 constructors XXREAL_0, REAL_1, NAT_1, PARTFUN1, NAT_D, AFINSQ_1, BINOP_2,
      INT_1, VALUED_1, RVSUM_1, RELSET_1, ORDINAL4, FUNCOP_1, FUNCT_7, NUMBERS;
 registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
      FINSEQ_1, AFINSQ_1, VALUED_0, FINSEQ_2, CARD_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve k,i for Nat;
reserve D for non empty set;

definition let D;

  let p be XFinSequence of D, q be FinSequence of D;
  pred p is_an_xrep_of q means
:: PRGCOR_2:def 1
  NAT c= D & (p.0)=len q & len q < len p &
  for i st 1<=i & i<=len q holds p.i=q.i;
end;

theorem :: PRGCOR_2:1
  for p being XFinSequence of D st NAT c= D &
  (p.0) is Nat & (p.0) in dom p holds p is_an_xrep_of (XFS2FS*(p));

definition
  let x be object, y be set, a,b,c be object;
  func IFLGT(x,y,a,b,c) -> object equals
:: PRGCOR_2:def 2
  a if x in y, b if x = y otherwise c;
end;

theorem :: PRGCOR_2:2
  for q being FinSequence of D, n being Nat st NAT c= D & n>len q
  ex p being XFinSequence of D st len p=n & p is_an_xrep_of q;

:: Non-overwriting program calculating inner product of vectors
::#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];
::   }

definition
  let a,b be XFinSequence of REAL;
  assume that
 b.0 is Nat and
 b.0 < len a;
  func inner_prd_prg(a,b) -> Real means
:: PRGCOR_2:def 3

  ex s being XFinSequence of REAL
  , n being Integer st len s=len a & s.0=0 & n= b.0 & (n<>0 implies for i being
  Nat st i<n holds s.(i+1)=s.i + (a.(i+1))*(b.(i+1)) ) & it=s.n;
end;

theorem :: PRGCOR_2:3
  for a being FinSequence of REAL, s being XFinSequence of REAL st
  s.0=0 & (for i st i<len a holds s.(i+1)=s.i+a.(i+1)) holds Sum a =s.(len a);

theorem :: PRGCOR_2:4
  for a being FinSequence of REAL holds ex s being XFinSequence of REAL
st len s=len a +1 & s.0=0 & (for i st i<len a holds s.(i+1)=s.i+a.(i+1)) & Sum
  a =s.(len a);

theorem :: PRGCOR_2:5
  for a,b being FinSequence of REAL, n being Nat st len a=len b & n>len
  a holds |(a,b)| = inner_prd_prg(FS2XFS*(a,n),FS2XFS*(b,n));

:: 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.

definition
  let b,c be XFinSequence of REAL,a be Real,m be Integer;
  pred m scalar_prd_prg c,a,b means
:: PRGCOR_2:def 4

  len c =m & len b =m & ex n being
Integer st c.0=b.0 & n=b.0 & (n<>0 implies for i being Nat st 1<=i & i<=n holds
  c.i=a*(b.i));
end;

theorem :: PRGCOR_2:6
  for b being non empty XFinSequence of REAL, a being Real,m being Nat
  st b.0 is Nat & len b=m & b.0 < m holds (ex c being XFinSequence of REAL st m
  scalar_prd_prg c,a,b)& for c being non empty XFinSequence of REAL st m
  scalar_prd_prg c,a,b holds (XFS2FS*(c))=a*(XFS2FS*(b));

:: Vector Calculation Program: Minus Vector
::#define V_SIZE 1024
::void vector_minus_prg(float c[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]= -b[i];
::         }
::        return;
::}
::The following definition is Logical-Model of the above program.

definition
  let b,c be XFinSequence of REAL,m be Integer;
  pred m vector_minus_prg c,b means
:: PRGCOR_2:def 5

  len c =m & len b =m & ex n being
  Integer st c.0=b.0 & n= b.0 & (n<>0 implies for i being Nat st 1<=i & i<=n
  holds c.i= -(b.i));
end;

theorem :: PRGCOR_2:7
  for b being non empty XFinSequence of REAL,m being Nat st b.0 is Nat &
len b=m & b.0 < m holds (ex c being XFinSequence of REAL st m vector_minus_prg
  c,b)& for c being non empty XFinSequence of REAL st m vector_minus_prg c,b
  holds (XFS2FS*(c))= -(XFS2FS*(b));

:: 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;
::}

definition
  let a,b,c be XFinSequence of REAL,m be Integer;
  pred m vector_add_prg c,a,b means
:: PRGCOR_2:def 6

  len c =m & len a=m & len b =m & ex
n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for i being Nat st 1<=i & i
  <=n holds c.i=(a.i)+(b.i) );
end;

theorem :: PRGCOR_2:8
  for a,b being non empty XFinSequence of REAL, m being Nat st b.0 is
  Nat & len a=m & len b=m & a.0=b.0 & b.0 < m holds (ex c being XFinSequence of
REAL st m vector_add_prg c,a,b)& for c being non empty XFinSequence of REAL st
  m vector_add_prg c,a,b holds (XFS2FS*(c))=(XFS2FS*(a))+(XFS2FS*(b));

:: 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;
::}

definition
  let a,b,c be XFinSequence of REAL,m be Integer;
  pred m vector_sub_prg c,a,b means
:: PRGCOR_2:def 7
  len c =m & len a=m & len b =m & ex n being Integer st c.0=b.0 & n=b.0 &
  (n<>0 implies for i being Nat st 1<=i & i <=n holds c.i=(a.i)-(b.i) );
end;

theorem :: PRGCOR_2:9
  for a,b being non empty XFinSequence of REAL, m being Nat st b.0 is
  Nat & len a=m & len b=m & a.0=b.0 & b.0 < m holds (ex c being XFinSequence of
REAL st m vector_sub_prg c,a,b) & for c being non empty XFinSequence of REAL st
  m vector_sub_prg c,a,b holds XFS2FS*(c)=XFS2FS*(a)-XFS2FS*(b);