:: Bubble Sort on SCM+FSA :: by JingChao Chen and Yatsuka Nakamura :: :: Received June 17, 1998 :: Copyright (c) 1998-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, EXTPRO_1, SCMFSA_2, AMI_1, SUBSET_1, SCMFSA7B, SCMFSA8C, AMI_3, CARD_1, AMISTD_2, SCMFSA8B, TURING_1, FSM_1, GRAPHSP, FUNCT_1, PARTFUN1, COMPLEX1, FUNCT_4, ARYTM_3, SF_MASTR, SCMFSA6C, SCMFSA6B, FUNCOP_1, RELAT_1, TARSKI, XBOOLE_0, XXREAL_0, AMISTD_1, CIRCUIT2, NAT_1, STRUCT_0, ARYTM_1, INT_1, FINSEQ_1, FINSEQ_2, SCMFSA6A, CLASSES1, VALUED_0, MSUALG_1, SCM_HALT, SCMBSORT, COMPOS_1; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, NAT_1, INT_1, RELAT_1, FINSEQ_1, FUNCT_1, COMPLEX1, FUNCT_2, PBOOLE, FUNCT_4, FINSEQ_2, FUNCT_7, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, FUNCOP_1, FINSUB_1, CARD_3, PARTFUN1, SCMFSA6B, SCMFSA6C, SCMFSA6A, SF_MASTR, SCMFSA8B, SCMFSA8C, CLASSES1, RFINSEQ, SCMFSA7B, NAT_D, SCM_HALT, XXREAL_0, SCMFSA_M; constructors SETWISEO, XXREAL_0, REAL_1, AMI_3, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA8B, SCMFSA8C, SCM_HALT, SCMFSA7B, AMISTD_2, NAT_D, CLASSES1, RELSET_1, DOMAIN_1, SFMASTR1, AMISTD_1, PBOOLE, PRE_POLY, SCMFSA_3, SCMFSA_7, SCMFSA_9, SCMFSA_2, XXREAL_2, MEMSTR_0, SCMFSA_1, SCMFSA_M, FUNCT_7, COMPOS_2, SCMFSA_X, SCMFSA9A; registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6C, SCMFSA7B, FINSET_1, SCMFSA8A, SCMFSA8B, SCMFSA_9, SCM_HALT, STRUCT_0, VALUED_0, ORDINAL1, RELAT_1, SCMFSA10, AMISTD_2, SCMFSA6A, COMPOS_1, SFMASTR1, FUNCT_4, EXTPRO_1, MEMSTR_0, AMI_3, COMPOS_0, AMISTD_1, SCMFSA_M, SCMFSA8C, SCMFSA9A; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve p for preProgram of SCM+FSA, ic for Instruction of SCM+FSA, i,j,k for Nat, fa,f for FinSeq-Location, a,b,da,db for Int-Location, la,lb for Nat; reserve p1,p2,q for Instruction-Sequence of SCM+FSA; ::$CT theorem :: SCMBSORT:2 for s be State of SCM+FSA,f be FinSeq-Location,a,b be Int-Location holds Exec(b:=(f,a), s).b = (s.f)/.|.s.a.|; theorem :: SCMBSORT:3 for s be State of SCM+FSA,f be FinSeq-Location,a,b be Int-Location holds Exec((f,a):=b, s).f = s.f+*(|.s.a.|,s.b); theorem :: SCMBSORT:4 for s be State of SCM+FSA,f be FinSeq-Location,m,n be Nat, a be Int-Location st m<>n+1 holds Exec(intloc m:=(f,a), Initialized s).intloc (n+1) =s.intloc (n+1); theorem :: SCMBSORT:5 for s be State of SCM+FSA,m,n be Nat,a be Int-Location st m<>n+1 holds Exec(intloc m:=a, Initialized s).intloc (n+1) =s.intloc (n+1) ; theorem :: SCMBSORT:6 for p being Instruction-Sequence of SCM+FSA for s be State of SCM+FSA, f be FinSeq-Location, a be read-write Int-Location holds IExec(Stop SCM+FSA,p,s).a =s.a & IExec(Stop SCM+FSA,p,s).f =s.f; reserve n for Nat; theorem :: SCMBSORT:7 ic in rng p & (ic = a:=b or ic = AddTo(a, b) or ic = SubFrom(a, b) or ic = MultBy(a, b) or ic = Divide(a, b)) implies a in UsedILoc p & b in UsedILoc p; theorem :: SCMBSORT:8 ic in rng p & (ic = a=0_goto la or ic = a>0_goto la) implies a in UsedILoc p; theorem :: SCMBSORT:9 ic in rng p & ( ic = b := (fa, a) or ic = (fa, a) := b) implies a in UsedILoc p & b in UsedILoc p; theorem :: SCMBSORT:10 ic in rng p & ( ic = b := (fa, a) or ic = (fa, a) := b) implies fa in UsedI*Loc p; theorem :: SCMBSORT:11 ic in rng p & (ic = a :=len fa or ic = fa :=<0,...,0>a) implies a in UsedILoc p; theorem :: SCMBSORT:12 ic in rng p & (ic = a :=len fa or ic = fa :=<0,...,0>a) implies fa in UsedI*Loc p; theorem :: SCMBSORT:13 for t being FinPartState of SCM+FSA,p being Program of SCM+FSA, x being set st dom t c= Int-Locations \/ FinSeq-Locations & x in dom t \/ UsedI*Loc p \/ UsedILoc p holds x is Int-Location or x is FinSeq-Location; theorem :: SCMBSORT:14 for i,k being Nat,t being FinPartState of SCM+FSA, p being Program of SCM+FSA, s1,s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & dom t c= Int-Locations \/ FinSeq-Locations & (for j holds IC Comput(p1,s1,j) in dom p & IC Comput(p2,s2,j) in dom p) & Comput(p1,s1,k).IC SCM+FSA = Comput(p2,s2,k).IC SCM+FSA & Comput(p1,s1,k) |(dom t \/ UsedI*Loc p \/ UsedILoc p) = Comput(p2,s2,k) |(dom t \/ UsedI*Loc p \/ UsedILoc p) holds Comput(p1,s1,i).IC SCM+FSA = Comput(p2,s2,i).IC SCM+FSA & Comput(p1,s1,i) |(dom t \/ UsedI*Loc p \/ UsedILoc p) = Comput(p2,s2,i) |(dom t \/ UsedI*Loc p \/ UsedILoc p); theorem :: SCMBSORT:15 for i,k being Nat,p being Program of SCM+FSA, s1,s2 being State of SCM+FSA st k <= i & p c= p1 & p c= p2 & (for j holds IC Comput(p1,s1,j) in dom p & IC Comput(p2,s2,j) in dom p) & Comput(p1,s1,k).IC SCM+FSA = Comput(p2,s2,k).IC SCM+FSA & Comput(p1,s1,k) | (UsedI*Loc p \/ UsedILoc p) = Comput(p2,s2,k) | (UsedI*Loc p \/ UsedILoc p) holds Comput(p1,s1,i).IC SCM+FSA = Comput(p2,s2,i).IC SCM+FSA & Comput(p1,s1,i) |(UsedI*Loc p \/ UsedILoc p) = Comput(p2,s2,i) |(UsedI*Loc p \/ UsedILoc p); ::$CT 7 theorem :: SCMBSORT:23 for i1,i2,i3 be Instruction of SCM+FSA holds card (i1 ";" i2 ";" i3)=6; ::$CT 2 theorem :: SCMBSORT:26 for I,J being Program of SCM+FSA, k being Nat, i being Instruction of SCM+FSA st k< card J & i = J. k holds (I ";" J).(card I +k) =IncAddr( i, card I ); theorem :: SCMBSORT:27 for I,J be Program of SCM+FSA, i be ins-loc-free Instruction of SCM+FSA st i <> halt SCM+FSA holds (I ";" i ";" J).card I = i; theorem :: SCMBSORT:28 for I,J be Program of SCM+FSA, i be Instruction of SCM+FSA holds (I ";" i ";" J).(card I+1) = goto(card I+2); ::$CT 3 theorem :: SCMBSORT:32 for p being Program of SCM+FSA,s being State of SCM+FSA holds UsedI*Loc p \/ UsedILoc p c= dom s; theorem :: SCMBSORT:33 for p being Instruction-Sequence of SCM+FSA for s be State of SCM+FSA,I be Program of SCM+FSA,f be FinSeq-Location holds Result(p +* I,Initialized s).f = IExec(I,p,s).f; :: set a0 = intloc 0; :: set a1 = intloc 1; :: set a2 = intloc 2; :: set a3 = intloc 3; :: set a4 = intloc 4; :: set a5 = intloc 5; :: set a6 = intloc 6; :: set initializeWorkMem= (a2:= a0) ";" (a3:= a0) ";" :: (a4:= a0) ";" (a5:= a0) ";" (a6:= a0); definition let f be FinSeq-Location; func bubble-sort f -> Program of SCM+FSA equals :: SCMBSORT:def 1 ( ((intloc 2):= (intloc 0)) ";" ((intloc 3):= (intloc 0)) ";" ((intloc 4):= (intloc 0)) ";" ((intloc 5):= (intloc 0)) ";" ((intloc 6):= (intloc 0)) ) ";" ((intloc 1):=len f) ";" Times((intloc 1), (intloc 2) := (intloc 1) ";" SubFrom(intloc 2,intloc 0) ";" ((intloc 3):=len f) ";" Times(intloc 2, (intloc 4):=(intloc 3) ";" SubFrom(intloc 3,intloc 0) ";" ((intloc 5):=(f,intloc 3)) ";" ((intloc 6):=(f,(intloc 4))) ";" SubFrom(intloc 6,intloc 5) ";" if>0(intloc 6, ((intloc 6):=(f,intloc 4)) ";" ((f,intloc 3):=(intloc 6)) ";" ((f,intloc 4):=(intloc 5)),Stop SCM+FSA) ) ); end; definition func Bubble-Sort-Algorithm -> Program of SCM+FSA equals :: SCMBSORT:def 2 bubble-sort fsloc 0; end; theorem :: SCMBSORT:34 for f being FinSeq-Location holds UsedILoc (bubble-sort f) = {intloc 0,intloc 1,intloc 2,intloc 3, intloc 4, intloc 5,intloc 6}; theorem :: SCMBSORT:35 for f being FinSeq-Location holds UsedI*Loc (bubble-sort f) = {f}; ::$CT 2 theorem :: SCMBSORT:38 for f being FinSeq-Location holds card (bubble-sort f) = 53; theorem :: SCMBSORT:39 for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P for f being FinSeq-Location, k being Nat st k < 53 holds Bubble-Sort-Algorithm.k= P.k; theorem :: SCMBSORT:40 bubble-sort (fsloc 0) is keepInt0_1 InitHalting; theorem :: SCMBSORT:41 for p be Instruction-Sequence of SCM+FSA for s be State of SCM+FSA holds s.(fsloc 0), IExec(bubble-sort (fsloc 0),p,s).(fsloc 0) are_fiberwise_equipotent & for i,j be Nat st i>=1 & j<=len (s.(fsloc 0)) & i= x2; theorem :: SCMBSORT:42 for i being Nat, s being State of SCM+FSA, P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P for w being FinSequence of INT st (Initialized ((fsloc 0) .--> w)) c= s holds IC Comput(P,s,i) in dom Bubble-Sort-Algorithm; theorem :: SCMBSORT:43 for p being Instruction-Sequence of SCM+FSA for s be State of SCM+FSA,t be FinSequence of INT st Initialize((intloc 0).-->1) +*(fsloc 0 .--> t) c= s & Bubble-Sort-Algorithm c= p ex u being FinSequence of REAL st t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result(p,s)).(fsloc 0) = u; theorem :: SCMBSORT:44 for w being FinSequence of INT holds Initialized ((fsloc 0) .--> w) is Bubble-Sort-Algorithm-autonomic; registration cluster Bubble-Sort-Algorithm -> halt-ending; end; theorem :: SCMBSORT:45 Bubble-Sort-Algorithm, Initialize((intloc 0).-->1) computes Sorting-Function;