:: Justifying the Correctness of Fibonacci Sequence and Euclid's :: Algorithm by Loop Invariant :: by JingChao Chen :: :: Received June 14, 2000 :: Copyright (c) 2000-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, AMI_1, SCMPDS_2, TURING_1, FUNCT_1, CARD_1, SCMFSA_7, RELAT_1, ARYTM_3, CARD_3, FSM_1, XXREAL_0, COMPLEX1, ARYTM_1, AMI_2, SCMPDS_5, SCMPDS_4, INT_1, SCMFSA6B, SCMFSA_9, UNIALG_2, SCMFSA7B, SCMP_GCD, SEMI_AF1, GRAPHSP, AMI_3, FINSEQ_1, SCPISORT, NAT_1, ORDINAL4, SFMASTR2, PRE_FF, FUNCT_4, CIRCUIT2, TARSKI, MSUALG_1, STRUCT_0, VALUED_1, SCMFSA8B, INT_2, SCPINVAR, PARTFUN1, EXTPRO_1, SCMFSA6C, COMPOS_1, MEMSTR_0; notations XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, VALUED_1, XCMPLX_0, RECDEF_1, FUNCT_4, INT_1, INT_2, NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, SCMPDS_2, SCMPDS_4, SCMPDS_6, SCMP_GCD, SCMPDS_5, SCMPDS_8, FUNCT_2, CARD_3, DOMAIN_1, FINSEQ_1, GR_CY_1, PRE_FF, SCPISORT, XXREAL_0; constructors DOMAIN_1, REAL_1, NAT_D, RECDEF_1, PRE_FF, MESFUNC1, GR_CY_1, SCM_1, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMP_GCD, SCMPDS_8, SCPISORT, BINOP_2, AMI_2, MEMSTR_0, RELSET_1; registrations FUNCT_1, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, CARD_3, STRUCT_0, SCMPDS_2, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMPDS_8, FINSEQ_1, CARD_1, VALUED_0, MEMSTR_0, COMPOS_1, AFINSQ_1, EXTPRO_1, FUNCT_4, COMPOS_0; requirements NUMERALS, REAL, SUBSET, ARITHM; begin :: Preliminaries reserve m,n for Element of NAT, i,j for Instruction of SCMPDS, I for Program of SCMPDS, a for Int_position; theorem :: SCPINVAR:1 (i ';' j ';' I). 0=i & (i ';' j ';' I). 1=j; theorem :: SCPINVAR:2 for a,b be Int_position holds ex f be Function of product the_Values_of SCMPDS,NAT st for s being State of SCMPDS holds (s.a = s.b implies f.s =0) & (s.a <> s.b implies f.s=max(|.s.a.|,|.s.b.|)); theorem :: SCPINVAR:3 ex f be Function of product the_Values_of SCMPDS,NAT st for s being State of SCMPDS holds (s.a >= 0 implies f.s =0) & (s.a < 0 implies f.s= -s.a); begin :: Computing directly the result of "while<0" program by loop-invariant reserve Q,U,P for Instruction-Sequence of SCMPDS; scheme :: SCPINVAR:sch 1 WhileLEnd { F(State of SCMPDS)-> Element of NAT, s() -> 0-started State of SCMPDS, P() -> Instruction-Sequence of SCMPDS, I() -> halt-free shiftable Program of SCMPDS, a() -> Int_position,i() -> Integer, P[set]}: F(Initialize IExec(while<0(a(),i(),I()),P(),s()))=0 & P[Initialize IExec(while<0(a(),i(),I()),P(),s())] provided for t be 0-started State of SCMPDS st P[t] holds F(t)=0 iff t.DataLoc(s().a(),i()) >= 0 and P[s()] and for t be 0-started State of SCMPDS,Q st P[t] & t.a()=s().a() & t.DataLoc(s().a(),i()) < 0 holds IExec(I(),Q,t).a()=t.a() & I() is_closed_on t,Q & I() is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t) & P[Initialize(IExec(I(),Q,t))]; begin :: An Example : Summing directly n integers by loop-invariant :: sum=Sum=x1+x2+...+xn definition let n, p0 be Element of NAT; func sum(n,p0) -> Program of SCMPDS equals :: SCPINVAR:def 1 (GBP:=0) ';' (intpos 1:=0) ';' ( intpos 2:=-n) ';' (intpos 3:=(p0+1)) ';' while<0(GBP,2,AddTo(GBP,1,intpos 3,0) ';' AddTo(GBP,2,1) ';' AddTo(GBP,3,1)); end; theorem :: SCPINVAR:4 for s being 0-started State of SCMPDS, I being halt-free shiftable Program of SCMPDS, a,b,c being Int_position,n,i,p0 be Element of NAT,f be FinSequence of INT st f is_FinSequence_on s,p0 & len f=n & s.b=0 & s.a=0 & s. intpos i=-n & s.c = p0+1 & (for t be 0-started State of SCMPDS, Q st (ex g be FinSequence of INT st g is_FinSequence_on s,p0 & len g=t.intpos i+n & t.b=Sum g & t.c = p0+1+ len g) & t.a=0 & t.intpos i < 0 & for i be Element of NAT st i > p0 holds t. intpos i=s.intpos i holds IExec(I,Q,t).a=0 & I is_closed_on t,Q & I is_halting_on t,Q & IExec(I,Q,t).intpos i=t.intpos i+1 & (ex g be FinSequence of INT st g is_FinSequence_on s,p0 & len g=t.intpos i+n+1 & IExec(I,Q,t).c = p0+1+len g & IExec(I,Q,t).b=Sum g) & for i be Element of NAT st i > p0 holds IExec(I,Q,t).intpos i=s.intpos i) holds IExec(while<0(a,i,I),P,s).b=Sum f & while<0(a,i,I) is_closed_on s,P & while<0(a,i,I) is_halting_on s,P; theorem :: SCPINVAR:5 for s being 0-started State of SCMPDS,n, p0 be Element of NAT, f be FinSequence of INT st p0 >= 3 & f is_FinSequence_on s,p0 & len f=n holds IExec(sum(n,p0),P,s).intpos 1=Sum f & sum(n,p0) is parahalting; begin :: Computing directly the result of "while>0" program by loop-invariant scheme :: SCPINVAR:sch 2 WhileGEnd { F(State of SCMPDS)-> Element of NAT, s() -> 0-started State of SCMPDS, P() -> Instruction-Sequence of SCMPDS, I() -> halt-free shiftable Program of SCMPDS, a() -> Int_position,i() -> Integer, P[set]}: F(Initialize IExec(while>0(a(),i(),I()),P(),s()))=0 & P[Initialize IExec(while>0(a(),i(),I()),P(),s())] provided for t be 0-started State of SCMPDS st P[t] holds F(t)=0 iff t.DataLoc(s().a(),i()) <= 0 and P[s()] and for t be 0-started State of SCMPDS,Q st P[t] & t.a()=s().a() & t.DataLoc( s().a(),i()) > 0 holds IExec(I(),Q,t).a()=t.a() & I() is_closed_on t,Q & I() is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t) & P[Initialize(IExec(I(),Q,t))]; begin :: An Example : Computing directly Fibonacci sequence by loop-invariant definition let n be Element of NAT; func Fib-macro(n) -> Program of SCMPDS equals :: SCPINVAR:def 2 (GBP:=0) ';' (intpos 1:=0) ';' (intpos 2:=1) ';' (intpos 3:=n) ';' while>0(GBP,3,((GBP,4):=(GBP,2)) ';' AddTo( GBP,2,GBP,1) ';' ((GBP,1):=(GBP,4)) ';' AddTo(GBP,3,-1)); end; theorem :: SCPINVAR:6 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a,f0,f1 being Int_position,n,i be Element of NAT st s.a=0 & s.f0=0 & s.f1=1 & s.intpos i=n & (for t be 0-started State of SCMPDS,Q for k be Element of NAT st n=t.intpos i+k & t.f0=Fib k & t.f1 = Fib (k+1) & t.a=0 & t. intpos i > 0 holds IExec(I,Q,t).a=0 & I is_closed_on t,Q & I is_halting_on t,Q & IExec(I,Q,t).intpos i=t.intpos i-1 & IExec(I,Q,t).f0=Fib (k+1) & IExec(I,Q,t).f1 = Fib (k+1+1)) holds IExec(while>0(a,i,I),P,s).f0=Fib n & IExec(while>0(a,i,I),P,s). f1=Fib (n+1) & while>0(a,i,I) is_closed_on s,P & while>0(a,i,I) is_halting_on s,P; theorem :: SCPINVAR:7 for s being 0-started State of SCMPDS, n be Element of NAT holds IExec(Fib-macro(n),P,s).intpos 1=Fib n & IExec(Fib-macro(n),P,s).intpos 2=Fib (n+1) & Fib-macro(n) is parahalting; begin :: The construction of while<>0 loop program :: while (a,i)<>0 do I definition let a be Int_position, i be Integer; let I be Program of SCMPDS; func while<>0(a,i,I) -> Program of SCMPDS equals :: SCPINVAR:def 3 (a,i)<>0_goto 2 ';' goto ( card I+2) ';' I ';' goto -(card I+2); end; begin :: The basic property of "while<>0" program theorem :: SCPINVAR:8 for a be Int_position,i be Integer,I be Program of SCMPDS holds card while<>0(a,i,I)= card I +3; theorem :: SCPINVAR:9 for a be Int_position,i be Integer,m be Element of NAT,I be Program of SCMPDS holds m < card I+3 iff m in dom while<>0(a,i,I); theorem :: SCPINVAR:10 for a be Int_position,i be Integer,I be Program of SCMPDS holds 0 in dom while<>0(a,i,I) & 1 in dom while<>0(a,i,I); theorem :: SCPINVAR:11 for a be Int_position,i be Integer,I be Program of SCMPDS holds while<>0(a,i,I). 0=(a,i)<>0_goto 2 & while<>0(a,i,I). 1= goto (card I +2) & while<>0(a,i,I). (card I+2)=goto -(card I+2); theorem :: SCPINVAR:12 for s being State of SCMPDS,I being Program of SCMPDS,a being Int_position, i being Integer st s.DataLoc(s.a,i) = 0 holds while<>0(a,i,I) is_closed_on s,P & while<>0(a,i,I) is_halting_on s,P; theorem :: SCPINVAR:13 for s being State of SCMPDS,I being Program of SCMPDS,a,c being Int_position, i being Integer st s.DataLoc(s.a,i) = 0 holds IExec(while<>0(a,i,I),P,Initialize s) = s +* Start-At((card I+3),SCMPDS) ; theorem :: SCPINVAR:14 for s being State of SCMPDS,I being Program of SCMPDS,a being Int_position, i being Integer st s.DataLoc(s.a,i) = 0 holds IC IExec(while<>0(a,i,I),P,Initialize s) = (card I + 3); theorem :: SCPINVAR:15 for s being State of SCMPDS,I being Program of SCMPDS,a,b being Int_position, i being Integer st s.DataLoc(s.a,i) = 0 holds IExec(while<>0(a,i,I),P,Initialize s).b = s.b; registration let I be shiftable Program of SCMPDS, a be Int_position,i be Integer; cluster while<>0(a,i,I) -> shiftable; end; registration let I be halt-free Program of SCMPDS, a be Int_position,i be Integer; cluster while<>0(a,i,I) -> halt-free; end; begin :: Computing directly the result of "while<>0" program by loop-invariant scheme :: SCPINVAR:sch 3 WhileNHalt { F(State of SCMPDS)-> Element of NAT, s() -> 0-started State of SCMPDS, P() -> Instruction-Sequence of SCMPDS, I() -> halt-free shiftable Program of SCMPDS, a() -> Int_position,i() -> Integer, P[set]}: while<>0(a(),i(),I()) is_closed_on s(),P() & while<>0(a(),i(),I()) is_halting_on s(),P() provided for t be 0-started State of SCMPDS st P[t] & F(t)=0 holds t.DataLoc(s().a(),i()) = 0 and P[s()] and for t be 0-started State of SCMPDS,Q st P[t] & t.a()=s().a() & t.DataLoc(s().a(),i()) <> 0 holds IExec(I(),Q,t).a()=t.a() & I() is_closed_on t,Q & I() is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t) & P[Initialize(IExec(I(),Q,t))]; scheme :: SCPINVAR:sch 4 WhileNExec { F(State of SCMPDS)-> Element of NAT, s() -> 0-started State of SCMPDS, P() -> Instruction-Sequence of SCMPDS, I() -> halt-free shiftable Program of SCMPDS, a() -> Int_position,i() -> Integer, P[set]}: IExec(while<>0(a(),i(),I()),P(),s()) = IExec(while<>0(a(),i(),I()),P(),Initialize IExec(I(),P(),s())) provided s().DataLoc(s().a(),i()) <> 0 and for t be 0-started State of SCMPDS st P[t] & F(t)=0 holds t.DataLoc(s().a(),i()) = 0 and P[s()] and for t be 0-started State of SCMPDS,Q st P[t] & t.a()=s().a() & t.DataLoc( s().a(),i()) <> 0 holds IExec(I(),Q,t).a()=t.a() & I() is_closed_on t,Q & I() is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t) & P[Initialize(IExec(I(),Q,t))]; scheme :: SCPINVAR:sch 5 WhileNEnd { F(State of SCMPDS)-> Element of NAT, s() -> 0-started State of SCMPDS, P() -> Instruction-Sequence of SCMPDS, I() -> halt-free shiftable Program of SCMPDS, a() -> Int_position,i() -> Integer, P[set]}: F(Initialize IExec(while<>0(a(),i(),I()),P(),s()))=0 & P[Initialize IExec(while<>0(a(),i(),I()),P(),s())] provided for t be 0-started State of SCMPDS st P[t] holds F(t)=0 iff t. DataLoc(s().a(),i()) = 0 and P[s()] and for t be 0-started State of SCMPDS,Q st P[t] & t.a()=s().a() & t.DataLoc( s().a(),i()) <> 0 holds IExec(I(),Q,t).a()=t.a() & I() is_closed_on t,Q & I() is_halting_on t,Q & F(Initialize IExec(I(),Q,t)) < F(t) & P[Initialize(IExec(I(),Q,t))]; theorem :: SCPINVAR:16 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a,b,c be Int_position,i,d be Integer st card I > 0 & s.a=d & s.b > 0 & s.c > 0 & s.DataLoc(d,i)=s.b-s.c & (for t be 0-started State of SCMPDS,Q st t.b > 0 & t.c > 0 & t.a=d & t.DataLoc(d,i)=t.b-t.c & t.b<>t.c holds IExec(I,Q,t).a=d & I is_closed_on t,Q & I is_halting_on t,Q & (t.b > t.c implies IExec(I,Q,t).b=t.b-t.c & IExec(I,Q,t).c = t.c) & (t.b <= t.c implies IExec(I,Q,t).c = t.c-t.b & IExec(I,Q,t) .b=t.b) & IExec(I,Q,t).DataLoc(d,i)= IExec(I,Q,t).b-IExec(I,Q,t).c) holds while<>0(a,i,I) is_closed_on s,P & while<>0(a,i,I) is_halting_on s,P & (s.DataLoc(s.a,i) <> 0 implies IExec(while<>0(a,i,I),P,s) = IExec(while<>0(a,i,I),P,Initialize IExec(I,P,s))); begin :: An example: computing Greatest Common Divisor (Euclid's algorithm) :: by loop-invariant :: gcd(x,y) < x=(GBP,1) y=(GBP,2),(GBP,3)=x-y > :: while x<>y do :: if x>y then x=x-y else y=y-x definition func GCD-Algorithm -> Program of SCMPDS equals :: SCPINVAR:def 4 (GBP:=0) ';' (GBP,3):=(GBP,1) ';' SubFrom(GBP,3,GBP,2) ';' while<>0(GBP,3, if>0(GBP,3,Load SubFrom(GBP,1,GBP, 2), Load SubFrom(GBP,2,GBP,1)) ';' (GBP,3):=(GBP,1) ';' SubFrom(GBP,3,GBP,2) ); end; theorem :: SCPINVAR:17 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a,b,c be Int_position,i,d be Integer st s.a=d & s.b > 0 & s.c > 0 & s.DataLoc(d,i)=s.b-s.c & (for t be 0-started State of SCMPDS,Q st t.b > 0 & t.c > 0 & t.a=d & t.DataLoc(d,i)=t.b-t.c & t.b<>t.c holds IExec(I,Q,t).a=d & I is_closed_on t,Q & I is_halting_on t,Q & (t.b > t.c implies IExec(I,Q,t).b=t.b-t.c & IExec(I,Q,t).c = t.c) & (t.b <= t.c implies IExec(I,Q,t).c = t.c-t.b & IExec(I,Q,t) .b=t.b) & IExec(I,Q,t).DataLoc(d,i)= IExec(I,Q,t).b-IExec(I,Q,t).c) holds IExec(while<>0(a,i,I),P,s).b = s.b gcd s.c & IExec(while<>0(a,i,I),P,s).c = s.b gcd s.c; theorem :: SCPINVAR:18 card GCD-Algorithm=12; theorem :: SCPINVAR:19 :: SCMP_GCD:18 for s being 0-started State of SCMPDS,x, y being Integer st s.intpos 1 = x & s.intpos 2 = y & x > 0 & y > 0 holds IExec(GCD-Algorithm,P,s).intpos 1 = x gcd y & IExec(GCD-Algorithm,P,s).intpos 2 = x gcd y & GCD-Algorithm is_closed_on s,P & GCD-Algorithm is_halting_on s,P;