:: Correctness of Non Overwriting Programs. {P}art {I} :: by Yatsuka Nakamura :: :: Received December 5, 2003 :: Copyright (c) 2003-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, SUBSET_1, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, INT_1, RELAT_1, NAT_1, FUNCT_1, NEWTON, FINSEQ_1, FUNCOP_1, TARSKI, PRGCOR_1; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FUNCT_1, FINSEQ_1, INT_1, RELSET_1, FUNCOP_1, PARTFUN1, NAT_1, NAT_D, NEWTON; constructors XXREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, BINARITH, RELSET_1, FUNCOP_1; registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON, VALUED_0; requirements REAL, NUMERALS, SUBSET, ARITHM; begin ::---------------------- ::---------------------- :: 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 restriction for non overwriting program. For statements, ::only the followings are allowed: substituting-statement, if-else-statement, ::for-statement(with break and without break), function(correct one)-call ::-statement and return-statement. :: Grammars of non overwriting program is like one of C-language. :: For type of variables, 'int','real","char" and "float" can be used, and ::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. :: 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 function-wise. We must use only ::correctness-proven functions to define a new function(to write a new ::program as a form of a function). :: Here, we present two program 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 do an area check of index of arrays used in one of the programs. ::--------- :: type correspondence: :: int .....> Integer :: float .....> Real :: char ......> Subset of A ::--------- :: statement correspondence: :: We use tr(statement_i) for translated logic formula corresponding :: to statement_i. :: i=j+k-l; ....> i=j+k-l :: i=j*k; ....> i=j*k :: x=y*z/s; ....> x=y*z/s :: statement_1;statement2;statement3;... :: .......> tr(statement_1)& tr(statement_2)& tr(statement_3)&... :: if (statement_1){statement_2;statement_3;...} :: .......> tr(statement_1) implies tr(statement_2)& tr(statement_3)&..; :: if (statement_1){statement_2;statement_3;...} else statement_4; :: .......> (tr(statement_1) implies tr(statement_2)& tr(statement_3)&..)& :: (not tr(statement_1) implies tr(statement_4)); :: for (i=1;i++;i<=n)statement_1; :: .......> for i being Integer st 1<=i & i<=n holds tr(statement_1); :: for (i=1;i++;i<=n){statement_1;statement_2;...;if (statement_3)break;} :: .......> (ex j being Integer st 1<=j & j<=n & :: (for i being Integer st 1<=i & i ex a being FinSequence of INT st len a=n & ...; :: float x[n+1] .....> ex x being FinSequence of REAL st len x=n & ...; :: Declaration of variables corresponds to existential statement. ::------ :: various correctness problem: :: 1. mathematical algorithm .....> a function is well defined in Mizar :: 2. semantic correctness .....> by theorems connecting it with :: other mathematical or computational concepts in Mizar :: 3. area check of variable of array .....> by a theorem checking :: the area, in Mizar :: 4. Is the translation to logic formula correct? :: ......> by other methods outside of Mizar :: 5. overflow problem .....> by other theorems, maybe in Mizar :: 6. error about float .....> avoid "=" sign in if clause, :: or corresponding float to other types not Real :: 7. translation of usual programs to non overwriting programs :: ......> by other methods outside of Mizar ::------ :: other comments: :: A concept of non overwriting is important, not only :: because of proving correctness, but because of debugging and :: safety of data. :: As memory is now cheap enough, it is wise to save all history of :: variables in a program. ::------------------------- ::------------------------- theorem :: PRGCOR_1:1 for n,m,k being Nat holds (n+k)-'(m+k)=n-'m; theorem :: PRGCOR_1:2 for n,k being Element of NAT st k>0 & n mod (2*k)>=k holds n mod (2*k)-k= n mod k & (n mod k) +k = n mod (2*k); theorem :: PRGCOR_1:3 for n,k being Element of NAT st k>0 & n mod (2*k)>=k holds n div k= (n div (2*k))*2+1; theorem :: PRGCOR_1:4 for n,k being Element of NAT st k>0 & n mod (2*k)0 & n mod (2*k)0 ex i being Element of NAT st (for k2 being Element of NAT st k2n; theorem :: PRGCOR_1:7 for i being Integer,f being FinSequence st 1<=i & i<=len f holds i in dom f; :: Overwrting program to divide n by m (n>=0&m>0),where division / used is :: special, because it is achieved by shifting a word. :: int idiv1_prg(int n,int m){ :: int sm,sn,pn,i,j; :: if(nn)break;} :: pn=0;sn=n;sm=sm/2; :: for (j=1;j<=i;j++){ :: if(sn>=sm){sn=sn-sm;sm=sm/2;pn=pn*2+1;} else {sm=sm/2;pn=pn*2;} :: } :: return pn; :: } :: Non overwrting program same as above, assuming n>=0 & m>0 :: int idiv1_prg(int n,int m){ :: int sm[n+1+1],sn[n+1+1],pn[n+1+1],i,j; :: if (nn){break;} :: } :: pn[i+1]=0;sn[i+1]=n; :: for (j=1;j<=i;j++){ :: if(sn[i+1-(j-1)]>=sm[i+1-j]){sn[i+1-j]=sn[i+1-(j-1)]-sm[i+1-j]; :: pn[i+1-j]=pn[i+1-(j-1)]*2+1;} :: else {sn[i+1-j]=sn[i+1-(j-1)]; pn[i+1-j]=pn[i+1-(j-1)]*2;} :: } :: return pn[1]; :: } definition let n,m be Integer; assume that n>=0 and m>0; func idiv1_prg(n,m) -> Integer means :: PRGCOR_1:def 1 ex sm,sn,pn being FinSequence of INT st len sm=n+1 & len sn=n+1 & len pn=n+1 & (nn)) & sm.(i+1)=sm.(i)*2 & sm.( i+1)>n & pn.(i+1)=0 & sn.(i+1)=n & (for j being Integer st 1<=j & j<=i holds ( sn.(i+1- (j- 1))>=sm.(i+1- j) implies sn.(i+1- j)=sn.(i+1- (j- 1))-sm.(i+1- j) & pn.(i+1- j)=pn.(i+1- (j- 1))*2+1 )& (not sn.(i+1- (j- 1))>=sm.(i+1- j) implies sn.(i+1- j)=sn.(i+1- (j- 1)) & pn.(i+1- j)=pn.(i+1- (j- 1))*2 ) )& it= pn.1 ); end; :: The following theorem is about array index area checking. :: Each index of an array appeared in the program is checked :: at the place just in front of the place the array is used, :: if it remains in the defined area of array. theorem :: PRGCOR_1:8 for n,m being Integer st n>=0 holds for sm,sn,pn being FinSequence of INT,i being Integer st len sm=n+1 & len sn=n+1 & len pn=n+1 & (not nn)) & sm.(i+1)=sm.(i)*2 & sm.(i+1)>n & pn.(i+1)=0 & sn.(i+1)= n & (for j being Integer st 1<=j & j<=i holds (sn.(i+1- (j- 1))>=sm.(i+1- j) implies sn.(i+1- j)=sn.(i+1- (j- 1))-sm.(i+1- j) & pn.(i+1- j)=pn.(i+1- (j- 1)) *2+1 )& (not sn.(i+1- (j- 1))>=sm.(i+1- j) implies sn.(i+1- j)=sn.(i+1- (j- 1)) & pn.(i+1- j)=pn.(i+1- (j- 1))*2 ) )& idiv1_prg(n,m)=pn.1 ) holds len sm=n+1 & len sn=n+1 & len pn=n+1 & (nn)) & i+1 in dom sm & i in dom sm & sm.(i+1)=sm.(i)*2 & sm.(i+1)>n & i+1 in dom pn & pn.(i+1)=0 & i+1 in dom sn & sn.(i+1)=n & (for j being Integer st 1<=j & j<=i holds i+1-(j-1) in dom sn & i+1-j in dom sm & (sn.(i+1- (j- 1))>=sm.(i+1- j) implies i+1-j in dom sn & i+1-j in dom sm & sn.(i+1- j)=sn.(i+1- (j- 1))-sm.(i+1- j) & i+1-j in dom pn & i+1-(j-1) in dom pn & pn.(i+1- j)=pn.(i+1- (j- 1))*2+1 )& (not sn.(i+1- (j - 1))>=sm.(i+1- j) implies i+1-j in dom sn & i+1-(j-1) in dom sn & sn.(i+1- j)= sn.(i+1- (j- 1)) & i+1-j in dom pn & i+1-(j-1) in dom pn & pn.(i+1- j)=pn.(i+1- (j- 1))*2 ) ) & 1 in dom pn & idiv1_prg(n,m) =pn.1 ); theorem :: PRGCOR_1:9 for n,m being Element of NAT st m>0 holds idiv1_prg(n qua Integer ,m qua Integer)=n div m; theorem :: PRGCOR_1:10 for n,m being Integer st n>=0 & m>0 holds idiv1_prg(n,m)=n div m; theorem :: PRGCOR_1:11 for n,m being Integer,n2,m2 being Element of NAT holds (m=0 & n2 =n & m2=m implies n div m=0 & n2 div m2=0)& (n>=0 & m>0 & n2=n & m2=m implies n div m =n2 div m2)& (n>=0 & m<0 & n2=n & m2= -m implies (m2*(n2 div m2)=n2 implies n div m =-(n2 div m2)) &(m2*(n2 div m2)<>n2 implies n div m =-(n2 div m2)-1))& (n<0 & m>0 & n2= -n & m2=m implies (m2*(n2 div m2)=n2 implies n div m =-(n2 div m2)) &(m2*(n2 div m2)<>n2 implies n div m =-(n2 div m2)-1))& (n<0 & m <0 & n2= -n & m2= -m implies n div m =n2 div m2); :: :: int idiv_prg(int n,int m){ :: int i; :: if (m==0){return 0;} :: if (n>=0 && m>0){return idiv1_prg(n,m);} :: if (n>=0 && m<0){ :: i= idiv1_prg(n,-m); :: if((-m)*i==n){return -i;} else{return -i-1;} :: } :: if (n<0 && m>0){ :: i= idiv1_prg(-n,m); :: if(m*i== -n){return -i;} else{return -i-1;} :: } :: return idiv1_prg(-n,-m); :: } :: :: One time writing program :: Same as above. definition let n,m be Integer; func idiv_prg(n,m) -> Integer means :: PRGCOR_1:def 2 ex i being Integer st (m=0 implies it=0)& (not m=0 implies (n>=0 & m>0 implies it= idiv1_prg(n,m))& (not ( n>=0 & m>0) implies (n>=0 & m<0 implies i=idiv1_prg(n,-m) & ((-m)*i=n implies it=-i )& ((-m)*i <> n implies it= -i-1 ) )& (not (n>=0 & m<0) implies (n<0 & m> 0 implies i=idiv1_prg(-n,m) & (m*i= -n implies it=-i )& (m*i <> -n implies it=- i-1 ) )& (not (n<0 & m>0) implies it=idiv1_prg(-n,-m) ) ) ) ); end; theorem :: PRGCOR_1:12 for n,m being Integer holds idiv_prg(n,m)=n div m;