:: Partial Correctness of a Factorial Algorithm :: by Adrian Jaszczak and Artur Korni{\l}owicz :: :: Received May 27, 2019 :: Copyright (c) 2019-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 NOMIN_1, NUMBERS, ZFMISC_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_1, NAT_1, ARYTM_3, PARTFUN1, XBOOLEAN, TARSKI, NOMIN_3, NOMIN_4, XCMPLX_0, NOMIN_2, PARTPR_1, PARTPR_2, NOMIN_5, REALSET1, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS, MARGREL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, FUNCOP_1, BINOP_1, XXREAL_0, XCMPLX_0, FUNCT_3, NEWTON, NOMIN_1, PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_3, NOMIN_4; constructors RELSET_1, INT_2, BINOP_1, FUNCOP_1, FUNCT_3, NEWTON, ENUMSET1, NOMIN_2, NOMIN_3, NOMIN_4; registrations ORDINAL1, RELSET_1, NOMIN_1, XCMPLX_0, NOMIN_2, NAT_1; requirements NUMERALS, BOOLE, SUBSET; begin definition let D be set; let f1,f2,f3 be BinominativeFunction of D; func PP_composition(f1,f2,f3) -> BinominativeFunction of D equals :: NOMIN_5:def 1 PP_composition(PP_composition(f1,f2),f3); end; definition let D be set; let f1,f2,f3,f4 be BinominativeFunction of D; func PP_composition(f1,f2,f3,f4) -> BinominativeFunction of D equals :: NOMIN_5:def 2 PP_composition(PP_composition(f1,f2,f3),f4); end; reserve D for non empty set; reserve f1,f2,f3,f4 for BinominativeFunction of D; reserve p,q,r,t,w for PartialPredicate of D; ::$N unconditional composition rule for 3 programs theorem :: NOMIN_5:1 <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*PP_inversion(q),f2,r*> is SFHT of D & <*PP_inversion(r),f3,w*> is SFHT of D implies <*p,PP_composition(f1,f2,f3),w*> is SFHT of D; ::$N unconditional composition rule for 4 programs theorem :: NOMIN_5:2 <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D & <*PP_inversion(q),f2,r*> is SFHT of D & <*PP_inversion(r),f3,w*> is SFHT of D & <*PP_inversion(w),f4,t*> is SFHT of D implies <*p,PP_composition(f1,f2,f3,f4),t*> is SFHT of D; reserve d,v,v1 for object; reserve V,A for set; reserve z for Element of V; reserve d1 for NonatomicND of V,A; reserve f for SCBinominativeFunction of V,A; reserve T for TypeSCNominativeData of V,A; theorem :: NOMIN_5:3 A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1 implies local_overlapping(V,A,d1,T,v).v1 = d1.v1; definition let x,y be object; assume x is Complex & y is Complex; func addition(x,y) -> Complex means :: NOMIN_5:def 3 ex x1,y1 being Complex st x1 = x & y1 = y & it = x1 + y1; func multiplication(x,y) -> Complex means :: NOMIN_5:def 4 ex x1,y1 being Complex st x1 = x & y1 = y & it = x1 * y1; end; definition let A; assume A is complex-containing; func addition(A) -> Function of [:A,A:],A means :: NOMIN_5:def 5 for x,y being object st x in A & y in A holds it.(x,y) = addition(x,y); func multiplication(A) -> Function of [:A,A:],A means :: NOMIN_5:def 6 for x,y being object st x in A & y in A holds it.(x,y) = multiplication(x,y); end; definition let V,A; let x,y be Element of V; func addition(A,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 7 lift_binary_op(addition(A),x,y); func multiplication(A,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 8 lift_binary_op(multiplication(A),x,y); end; theorem :: NOMIN_5:4 for i,j being Element of V holds A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom addition(A,i,j) implies for x,y being Complex st x = d1.i & y = d1.j holds addition(A,i,j).d1 = x + y; theorem :: NOMIN_5:5 for i,j being Element of V holds A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom multiplication(A,i,j) implies for x,y being Complex st x = d1.i & y = d1.j holds multiplication(A,i,j).d1 = x * y; :: Pseudocode of n! :: :: i := val.1 :: j := val.2 :: n := val.3 :: s := val.4 :: { s == i! } :: while ( i <> n ) :: i := i + j :: s := s * i :: return s :: { n == i && s == i! } :: :: where :: val.1 = 0, :: val.2 = 1, :: val.3 - the number n the factorial of which we compute, :: val.4 = 1 :: are input data from the environment, :: and loc/.1 = i, loc/.2 = j, loc/.3 = n, loc/.4 = s. reserve loc for V-valued Function; reserve val for Function; definition let V,A,loc; func factorial_loop_body(A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 9 PP_composition( SC_assignment(addition(A,loc/.1,loc/.2),loc/.1), SC_assignment(multiplication(A,loc/.4,loc/.1),loc/.4) ); end; definition let V,A,loc; func factorial_main_loop(A,loc) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 10 PP_while(PP_not(Equality(A,loc/.1,loc/.3)),factorial_loop_body(A,loc)); end; definition let V,A,loc,val; func factorial_var_init(A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 11 PP_composition( SC_assignment(denaming(V,A,val.1), loc/.1), SC_assignment(denaming(V,A,val.2), loc/.2), SC_assignment(denaming(V,A,val.3), loc/.3), SC_assignment(denaming(V,A,val.4), loc/.4) ); end; definition let V,A,loc,val; func factorial_main_part(A,loc,val) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 12 PP_composition( factorial_var_init(A,loc,val), factorial_main_loop(A,loc) ); end; definition let V,A,loc,val,z; func factorial_program(A,loc,val,z) -> SCBinominativeFunction of V,A equals :: NOMIN_5:def 13 PP_composition( factorial_main_part(A,loc,val), SC_assignment(denaming(V,A,loc/.4),z) ); end; reserve n0 for Nat; definition let V,A,val,n0,d; pred valid_factorial_input_pred V,A,val,n0,d means :: NOMIN_5:def 14 ex d1 being NonatomicND of V,A st d = d1 & { val.1, val.2, val.3, val.4 } c= dom d1 & d1.(val.1) = 0 & d1.(val.2) = 1 & d1.(val.3) = n0 & d1.(val.4) = 1; end; definition let V,A,val,n0; func valid_factorial_input(V,A,val,n0) -> SCPartialNominativePredicate of V,A means :: NOMIN_5:def 15 dom it = ND(V,A) & for d being object st d in dom it holds (valid_factorial_input_pred V,A,val,n0,d implies it.d = TRUE) & (not valid_factorial_input_pred V,A,val,n0,d implies it.d = FALSE); end; registration let V,A,val,n0; cluster valid_factorial_input(V,A,val,n0) -> total; end; definition let V,A,z,n0,d; pred valid_factorial_output_pred A,z,n0,d means :: NOMIN_5:def 16 ex d1 being NonatomicND of V,A st d = d1 & z in dom d1 & d1.z = n0!; end; definition let V,A,z,n0; func valid_factorial_output(A,z,n0) -> SCPartialNominativePredicate of V,A means :: NOMIN_5:def 17 dom it = {d where d is TypeSCNominativeData of V,A: d in dom denaming(V,A,z)} & for d being object st d in dom it holds (valid_factorial_output_pred A,z,n0,d implies it.d = TRUE) & (not valid_factorial_output_pred A,z,n0,d implies it.d = FALSE); end; definition let V,A,loc,n0,d; pred factorial_inv_pred A,loc,n0,d means :: NOMIN_5:def 18 ex d1 being NonatomicND of V,A st d = d1 & { loc/.1, loc/.2, loc/.3, loc/.4 } c= dom d1 & d1.(loc/.2) = 1 & d1.(loc/.3) = n0 & ex I,S being Nat st I = d1.(loc/.1) & S = d1.(loc/.4) & S = I!; end; definition let V,A,loc,n0; func factorial_inv(A,loc,n0) -> SCPartialNominativePredicate of V,A means :: NOMIN_5:def 19 dom it = ND(V,A) & for d being object st d in dom it holds (factorial_inv_pred A,loc,n0,d implies it.d = TRUE) & (not factorial_inv_pred A,loc,n0,d implies it.d = FALSE); end; registration let V,A,loc,n0; cluster factorial_inv(A,loc,n0) -> total; end; definition let V,loc,val; pred loc,val are_compatible_wrt_4_locs means :: NOMIN_5:def 20 val.4 <> loc/.3 & val.4 <> loc/.2 & val.4 <> loc/.1 & val.3 <> loc/.2 & val.3 <> loc/.1 & val.2 <> loc/.1; end; theorem :: NOMIN_5:6 V is non empty & A is_without_nonatomicND_wrt V & loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct & loc,val are_compatible_wrt_4_locs implies <* valid_factorial_input(V,A,val,n0), factorial_var_init(A,loc,val), factorial_inv(A,loc,n0) *> is SFHT of ND(V,A); theorem :: NOMIN_5:7 V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct implies <* factorial_inv(A,loc,n0), factorial_loop_body(A,loc), factorial_inv(A,loc,n0) *> is SFHT of ND(V,A); ::$CT theorem :: NOMIN_5:9 V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct implies <* factorial_inv(A,loc,n0), factorial_main_loop(A,loc), PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0)) *> is SFHT of ND(V,A); theorem :: NOMIN_5:10 V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct & loc,val are_compatible_wrt_4_locs implies <* valid_factorial_input(V,A,val,n0), factorial_main_part(A,loc,val), PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0)) *> is SFHT of ND(V,A); theorem :: NOMIN_5:11 V is non empty & A is_without_nonatomicND_wrt V & (for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T) implies PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0)) ||= SC_Psuperpos(valid_factorial_output(A,z,n0),denaming(V,A,loc/.4),z); theorem :: NOMIN_5:12 V is non empty & A is_without_nonatomicND_wrt V & (for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T) implies <* PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0)), SC_assignment(denaming(V,A,loc/.4),z), valid_factorial_output(A,z,n0) *> is SFHT of ND(V,A); theorem :: NOMIN_5:13 (for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T) implies <* PP_inversion(PP_and(Equality(A,loc/.1,loc/.3),factorial_inv(A,loc,n0))), SC_assignment(denaming(V,A,loc/.4),z), valid_factorial_output(A,z,n0) *> is SFHT of ND(V,A); ::$N Partial correctness of a FACTORIAL algorithm theorem :: NOMIN_5:14 V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc/.1, loc/.2, loc/.3, loc/.4 are_mutually_distinct & loc,val are_compatible_wrt_4_locs & (for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T) implies <* valid_factorial_input(V,A,val,n0), factorial_program(A,loc,val,z), valid_factorial_output(A,z,n0) *> is SFHT of ND(V,A);