《The for (going up) macro instruction》由会员分享，可在线阅读，更多相关《The for (going up) macro instruction（7页珍藏版）》请在金锄头文库上搜索。
1、JOURNAL OF FORMALIZED MATHEMATICSVolume 10, Released 1998, Published 2003Inst. of Computer Science, Univ. of BiaystokThe for (going up) Macro InstructionPiotr RudnickiUniversity of AlbertaEdmontonSummary. We define a for type (going up) macro instruction in terms of the whilemacro. This gives an ite
2、rative macro with an explicit control variable. The for macro is usedto define a macro for the selection sort acting on a finite sequence location of SCMFSA. Onthe way, a macro for finding a minimum in a section of an array is defined.MML Identifier: SFMASTR3.WWW: http:/mizar.org/JFM/Vol10/sfmastr3.
3、htmlThe articles 24, 35, 7, 26, 9, 8, 18, 25, 32, 6, 33, 36, 37, 12, 14, 13, 11,19, 5, 17, 27, 23, 10, 15, 34, 20, 28, 31, 29, 30, 3, 22, 4, 2, 1, 16,and 21 provide the notation and terminology for this paper.1. GENERAL PRELIMINARIESOne can prove the following two propositions:(1) Let X be a set, p
4、be a permutation of X, and x, y be elements of X. Then p+(x, p(y)+(y, p(x) is a permutation of X.(2) Let f be a function and x, y be sets. Suppose x dom f and y dom f. Then there exists apermutation p of dom f such that f +(x, f(y)+(y, f(x)= f p.Let A be a finite non empty real-membered set. Then in
5、fA can be characterized by the condition:(Def. 1) infA A and for every real number k such that k A holds infA k.We introduce minA as a synonym of infA.Let X be a finite non empty natural-membered set. Observe that minX is integer.Let F be a finite sequence of elements of Z and let m, n be natural nu
6、mbers. Let us assumethat 1 m and m n and n lenF. The functor minnm F yields a natural number and is defined asfollows:(Def. 3)1 There exists a finite non empty subset X of Z such that X = rngF(m),.,F(n) and(minnm F)+1 =(minX)curlyleftF(m),.,F(n)+m.We follow the rules: F, F1 are finite sequences of e
7、lements of Z and k, m, n, m1 are naturalnumbers.We now state two propositions:1 The definition (Def. 2) has been removed.1 c Association of Mizar UsersTHE for (GOING UP) MACRO INSTRUCTION 2(3) Suppose 1 m and m n and n lenF. Then m1 = minnm F if and only if the followingconditions are satisfied:(i)
8、m m1,(ii) m1 n,(iii) for every natural number i such that m i and i n holds F(m1) F(i), and(iv) for every natural number i such that m i and i b then I else J is good.The following propositions are true:(13) UsedIntLoc(if a1 b1 then I else J)=a1,b1UsedIntLoc(I)UsedIntLoc(J).(14) If I does not destro
9、y a1, then while b1 0 do I does not destroy a1.(15) If c1 negationslash= a1 and I does not destroy c1 and J does not destroy c1, then if a1 b1 then I else Jdoes not destroy c1.THE for (GOING UP) MACRO INSTRUCTION 33. THE for-up MACRO INSTRUCTIONLet a, b, c be integer locations, let I be a macro inst
10、ruction, and let s be a state of SCMFSA. Thefunctor StepForUp(a,b,c,I,s) yields a function from N into (the object kind of SCMFSA) and isdefined as follows:(Def. 6) StepForUp(a,b,c,I,s)=StepWhile0(a2,I; AddTo(a,intloc(0); SubFrom(a2,intloc(0),s+(a2,(s(c)s(b)+1)+(a,s(b), where a2 = 1st -RWNotIn(a,b,c
11、UsedIntLoc(I).We now state several propositions:(16) If s(intloc(0)= 1, then (StepForUp(a,b1,c1,I,s)(0)(intloc(0)= 1.(17) (StepForUp(a,b1,c1,I,s)(0)(a)= s(b1).(18) If a negationslash= b1, then (StepForUp(a,b1,c1,I,s)(0)(b1)= s(b1).(19) If a negationslash= c1, then (StepForUp(a,b1,c1,I,s)(0)(c1)= s(c
12、1).(20) If a negationslash= d1 and d1 UsedIntLoc(I), then (StepForUp(a,b1,c1,I,s)(0)(d1)= s(d1).(21) (StepForUp(a,b1,c1,I,s)(0)(f)= s(f).(22) Suppose s(intloc(0) = 1. Let a2 be a read-write integer location. If a2 =1st -RWNotIn(a,b1,c1UsedIntLoc(I), then IExec(a2:=c1); SubFrom(a2,b1); AddTo(a2,intlo
13、c(0); (a:=b1),s)harpoonuprightD=(s+(a2,(s(c1)s(b1)+1)+(a,s(b1)harpoonuprightD, where D = Int-LocationsFinSeq-Locations.Let a, b, c be integer locations, let I be a macro instruction, and let s be a state of SCMFSA. Wesay that ProperForUpBody a, b, c, I, s if and only if:(Def. 7) For every natural nu
14、mber i such that i 0 if and onlyif k 0 do (I; AddTo(a,intloc(0); SubFrom(a2,intloc(0), where a2 = 1st -RWNotIn(a,b,cUsedIntLoc(I).The following proposition is true(28) a1,b1,c1UsedIntLoc(I) UsedIntLoc(for-up(a1,b1,c1,I).Let a be a read-write integer location, let b, c be integer locations, and let I
15、 be a good macroinstruction. One can check that for-up(a,b,c,I) is good.We now state four propositions:(29) If a negationslash= a1 and a1 negationslash= 1st -RWNotIn(a,b1,c1UsedIntLoc(I) and I does not destroy a1,then for-up(a,b1,c1,I) does not destroy a1.(30) Suppose s(intloc(0) = 1 and s(b1) s(c1). Then for every x such that x negationslash= a and x b1,c1UsedIntLoc(I) holds (IExec(for-up(a,b1,c1,I),s)(x)= s(x) and for every f holds(IExec(for-up(a,b1,c1,I),s)(f)= s(f).(31) Suppose s(intloc(0)=1 but k =(s(c1)s(b1)+1 but ProperForUpBody a, b1, c1, I1, s orI1 is parahalting. The
