:: 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 begin definition let D be non empty set ; let p be XFinSequence of ; let q be FinSequence of D; predp is_an_xrep_of q means :Def1: :: PRGCOR_2:def 1 ( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds p . i = q . i ) ); end; :: deftheorem Def1 defines is_an_xrep_of PRGCOR_2:def_1_:_ for D being non empty set for p being XFinSequence of for q being FinSequence of D holds ( p is_an_xrep_of q iff ( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds p . i = q . i ) ) ); theorem :: PRGCOR_2:1 for D being non empty set for p being XFinSequence of st NAT c= D & p . 0 is Nat & p . 0 in len p holds p is_an_xrep_of XFS2FS* p proofend; definition let x, y, a, b, c be set ; func IFLGT (x,y,a,b,c) -> set equals :Def2: :: PRGCOR_2:def 2 a if x in y b if x = y otherwise c; correctness coherence ( ( x in y implies a is set ) & ( x = y implies b is set ) & ( not x in y & not x = y implies c is set ) ); consistency for b1 being set st x in y & x = y holds ( b1 = a iff b1 = b ); ; end; :: deftheorem Def2 defines IFLGT PRGCOR_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 ) ); theorem Th2: :: PRGCOR_2:2 for D being non empty set for q being FinSequence of D for n being Nat st NAT c= D & n > len q holds ex p being XFinSequence of st ( len p = n & p is_an_xrep_of q ) proofend; :: 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 Real means :Def3: :: PRGCOR_2:def 3 ex s being XFinSequence of ex 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 ); existence ex b1 being Real ex s being XFinSequence of ex 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))) ) & b1 = s . n ) proofend; uniqueness for b1, b2 being Real st ex s being XFinSequence of ex 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))) ) & b1 = s . n ) & ex s being XFinSequence of ex 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))) ) & b2 = s . n ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines inner_prd_prg PRGCOR_2:def_3_:_ for a, b being XFinSequence of st b . 0 is Nat & b . 0 < len a holds for b3 being Real holds ( b3 = inner_prd_prg (a,b) iff ex s being XFinSequence of ex 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))) ) & b3 = s . n ) ); theorem Th3: :: PRGCOR_2:3 for a being FinSequence of REAL for s being XFinSequence of st s . 0 = 0 & ( for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ) holds Sum a = s . (len a) proofend; theorem :: PRGCOR_2:4 for a being FinSequence of REAL ex s being XFinSequence of st ( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) ) proofend; theorem :: PRGCOR_2:5 for a, b being FinSequence of REAL for n being Nat st len a = len b & n > len a holds |(a,b)| = inner_prd_prg ((FS2XFS* (a,n)),(FS2XFS* (b,n))) proofend; :: 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 ; let a be Real; let m be Integer; predm scalar_prd_prg c,a,b means :Def4: :: 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; :: deftheorem Def4 defines scalar_prd_prg PRGCOR_2:def_4_:_ for b, c being XFinSequence of for a being Real for m being Integer holds ( m scalar_prd_prg c,a,b iff ( 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) ) ) ) ); theorem :: PRGCOR_2:6 for b being non empty XFinSequence of for a being Real for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds ( ex c being XFinSequence of st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of st m scalar_prd_prg c,a,b holds XFS2FS* c = a * (XFS2FS* b) ) ) proofend; :: 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 ; let m be Integer; predm vector_minus_prg c,b means :Def5: :: 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; :: deftheorem Def5 defines vector_minus_prg PRGCOR_2:def_5_:_ for b, c being XFinSequence of for m being Integer holds ( m vector_minus_prg c,b iff ( 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) ) ) ) ); theorem :: PRGCOR_2:7 for b being non empty XFinSequence of for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds ( ex c being XFinSequence of st m vector_minus_prg c,b & ( for c being non empty XFinSequence of st m vector_minus_prg c,b holds XFS2FS* c = - (XFS2FS* b) ) ) proofend; :: 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 ; let m be Integer; predm vector_add_prg c,a,b means :Def6: :: 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; :: deftheorem Def6 defines vector_add_prg PRGCOR_2:def_6_:_ for a, b, c being XFinSequence of for m being Integer holds ( m vector_add_prg c,a,b iff ( 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) ) ) ) ); theorem :: PRGCOR_2:8 for a, b being non empty XFinSequence of for 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 st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) ) proofend; :: 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 ; let m be Integer; predm vector_sub_prg c,a,b means :Def7: :: 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; :: deftheorem Def7 defines vector_sub_prg PRGCOR_2:def_7_:_ for a, b, c being XFinSequence of for m being Integer holds ( m vector_sub_prg c,a,b iff ( 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) ) ) ) ); theorem :: PRGCOR_2:9 for a, b being non empty XFinSequence of for 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 st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of st m vector_sub_prg c,a,b holds XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) ) proofend;