 J. Software Engineering & Applications, 2009, 2: 195-199 doi:10.4236/jsea.2009.23026 Published Online October 2009 (http://www.SciRP.org/journal/jsea) Copyright © 2009 SciRes JSEA 195Formal Derivation of the Combinatorics Problems with PAR Method Lingyu SUN1, Yatian SUN2 1Department of Compute r Science, Jinggangshan University, Ji’an, China; 2School of Chemistry and Materials Science, University of Science and Technology of China, Hefei, China. Email: sunlingyu@jgsu.edu.cn Received May 12th, 2009; revised June 13th, 2009; accepted June 17th, 2009. ABSTRACT Partition-and-Recur (PAR) method is a simple and useful formal method. It can be used to design and testify algo-rithmic programs. In this paper, we propose that PAR method is an effective formal method on solving combinatorics problems. Furthermore, we formally derive combinatorics problems by PAR method, which cannot only simplify the process of algorithmic program's designing, but also improve its automatization, standardization and correctness. We develop algorithms for two typical combinatorics problems, the number of string scheme and the number of error per-mutation scheme. Lastly, we obtain accurate C++ programs which are transformed by automatic transforming system of PAR platform. Keywords: PAR Method, Formal Derivation, Combinator ics, Algorithmic Programs 1. Introduction Computer Science is a science of developing correct and efficient algorithms. Its main research object is discrete data handled by computer. As long as the algorithm in-volves iterant calculation, each traditional strategy of algorithm design can embody the principle of partition and recurrence. Partition is a general approach for deal-ing with complicated objects and is typically used in di-vide-and-conquer approach. Recurrence is used in algo-rithm analysis and dynamic programming approach. PAR method is a unified approach of developing efficient al-gorithmic programs and its key idea is partition and re-currence. Using PAR method, we begin from the formal specification of a specified problem, partition the prob-lem into a couple of sub problems, and develop an effi-cient and correct algorith m represented by recurrence and initiation [1-3]. Combinatorics is a science of studying discrete objects. In general, it includes basic theories, counting methods and algorithms widely used in combination. Combina-torics algorithms are based on combinatorics and make people feel that computer may have its own thought. However, many programming teaching materials can only present combinatorics algorithms but cannot pro-vide the formal derived procedures that design the spe-cific algorithms from the unresolved combinatorics problems. So algorithm designers cannot understand the essence of algorithms and cannot improve their capabil-ity of algorithm design . PAR method embodies rich mathematic ideology, it provides many powerful tools and appropriate develop-ing environment. We can avoid making a choice among various design methods by adopting PAR method to de-velop combinatory algorithms. It can also change many creative labor to mechanized labor, and can finally im-prove algorithmic programs design’s automatization, standardization and correctness [5,6]. In this paper, we propose that PAR method is an effec-tive formal method on solving combinatorics problems. We formally derive several typical algorithms of combi-natorics problems by PAR method, which cannot only solve the above problems, but also can assure their cor-rectness on logic. These combinatorics problem instances include the number of string scheme, the number of error permutation scheme, maximum summary , the longest common subsequence , minimum spanning tree [4,7] and the Knapsack problem , etc. Because of the lim-ited space, we only describe the whole developing proc-ess of two specific combinatorics problem instances, the number of string scheme and the number of error permu-tation scheme, which are derived by PAR methods. 2. The Developing Steps of the Number of String Scheme Derived by PAR Methods Suppose that A=,,,abcd , n is given, and we want to Formal Derivation of the Combinatorics Problems with PAR Method 196 select n elements to compose string, in which element a and b cannot be adjacent elements. How many schemes are there in a string with n elements?  2.1 The Formal Function Specification of the Number of String Scheme PQ: Given integer n, set A=,,,abcd , string S stores n elements of set A. PR: Let  Stringn=SS k=aS k=bS k 1cSk dkn   and  ,:FSij ij 1ba , then :..1nSjjab Sj..j(: ():ZNSSString nn (:1: ))jjnSjj abSjj ba  = {According to the definition of } ,FSi(: ():(,1))NSSString nFS = {equivalent transformation of quantifier} (:() (,1):1)SS StringnFS (1) 2.2 Partition the Problem Based on the Post-Assertion We partition computing Zn into computing Xn and Yn , each of that has the same structure with Zn. (:() (,1)XSSString nFSn  ( ):1)SaSb (2) In Equation (2), Xn denote the number of n elements’ string scheme that element a and b cannot be adjacent elements and the initial element is a or b. (:() (,1)YSSString nF Sn  ( ):1)ScSd (3) In Equation (3), Yn denote the number of n elements’ string scheme that element a and b cannot be adjacent elements and the initial element is c or d. (:() (,1):1)ZSSString nF Sn  (:() (,1)SSString nFS  () :1)SaSbScSd  ={Range Disjunction} ( :()(,1) ():1)SSStringnF SSaSb(:()(,1)() :1)SSString nFSScSd = {According to the definition of Xn and Yn} XYnn (4) According to the equation (4), we can partition com-puting Zn into computing Xn and Yn. 2.3 Construct the Recurrence Relation Suppose Xn-1 denotes the number of n-1 elements’ string scheme that satisfy the condition and the initial element is a or b. Yn-1 denotes the number of n-1 elements’ string scheme that satisfy the condition and the initial element is c or d. (:() (,1)XSSStringnFSn  ( ):1)SaSb  ( :()(,1) (SSString nF SS  )(aSbS ):1)aS bS cSd = {Range Disjunction} (:( )(,1)()SSString nFSSS ( ):1)SaSb  (:( )(,1)()SSString nF SSa ():1)ScSd  (:( )(,1)()SSString nF SSb ():1)ScSd  = {According to the definition of } ,FSi(:() ()(,2)SS StringnSSFS ( ):1)SaSb  (:() ()(,2)SSString nSaFS ():1)ScSd  (:() ()(,2)SSString nSbFS ():1)ScSd  = {According to the definition of Xn-1 and Yn-1 } 21XYn 1n (5) According to the equation (5), we can partition com-puting Xn into computing Xn-1 and 2×Yn-1. (:() (,1)YSSString nFSn  ( ):1)ScSd  ( :()(,1) (SSString nF SS  )( cSd SaS   ):1)bS cS d Copyright © 2009 SciRes JSEA Formal Derivation of the Combinatorics Problems with PAR Method 197 = {Range Disjunction} (:( )(,1)()SSString nF SScSd ( ):1)SaSb (:( )(,1)()SSString nF SScSd ():1)ScSd = {Range Disjunction} (:( )(,1)( )SSString nFSSc ( ):1)SaSb (:( )(,1)( )SS StringnFSSd ( ):1)SaSb (:( )(,1)( )SSString nF SSc ():1)ScSd (:( )(,1)( )SS StringnFSSd ():1)ScSd = {According to the definition of ,FSi } (:() ()(,2)SS StringnScFS ( ):1)SaSb 1n (:() ()(,2)SSString nSdF S ( ):1)SaSb (:() ()(,2)SS StringnScFS ():1)ScSd (:() ()(,2)SSString nSdF S ():1)ScSd = {According to the definition of Xn-1 and Yn-1 } 221XYn (6) According to the equation (6), we can also partition computing Yn into computing 2×Xn-1 and 2×Yn-1. 2.4 Developing Loop Invariant Suppose variant x stores the value of Xi, variant u stores the value of Xi+1, variant y stores the value of Yi, variant v stores the value of Yi+1, variant z stores the value of Zi, where X1=2, Y1=2, Z1=4. LI: 11xXuXyYvYzZiiii (1 )ini 2.5 Developing Corresponding RADL Program The Recurrence-based Algorithm Design Language (RADL) program of the number of string scheme, derived by PAR methods, is shown in Algorithm 1. By the auto-matic program transforming system of PAR platform, we can get the Abstract Programming Language (APLA) program of the number of string scheme which is trans-formed from the RADL program and is shown in Algo-rithm 2. Finally, we transform the APLA program of the number of string scheme to C++ program, which can get accurate running result. Algorithm 1 (The RADL program of string scheme) |[in n:integer; i:integer; x,y,u,v: integer; out z:integer;]| {PQ∧PR} Begin: i=1++1; x=2; y=2; z=4; A_I: 1xxiuxiyyi  11vyi zziin Termination: i=n; Recur: u=x+2*y; v=2*x+2*y; z=u+v; x=u; y=v; End. Algorithm 2 (The APLA program of string scheme) var: n:integer; i:integer; x,y,u,v: integer; z:integer; begin: write(“Please input integer n value”); read(n); i:=1;x:=2;y:=2;z:=4; do (﹁(i=n)) → u:=x+2*y; v:=2*x+2*y; z:=u+v x:=u; y:=v; i:=i+1; od write(“The Number of string scheme:”, z); end. 3. The Developing Steps of the Number of Error Permutation Scheme Derived by PAR Methods Suppose that the original arrange scheme is A =[a1…ai…an], which is satisfied with each element is different. We want to interlace n elements of original permutation scheme A to compose new permutation scheme B, in which each element cannot be the same position in A. How many schemes are there in error per-mutation with n elements?  3.1 The Formal Function Specification of the Number of Error Permutation Scheme PQ: Given the original permutation scheme A =[a1…ai…an] , which is satisfied with(,:ij Copyright © 2009 SciRes JSEA Formal Derivation of the Combinatorics Problems with PAR Method 198 (1) : ([][]))ijn Ai Aj (){ |Perm ABB1,, }ijk nj k  . PR: Let [][] [][]jA iBjBk, then ::1:DNBB PermAn jj nBjAj = {equivalent transformation of quantifier} ::BB PermAj1:j nBjAj:1 =:1 :iinBnAitrue 1:jnBjA j::BBPermAj':1 :iinB  :1nAi (7) 3.2 Partition the Problem Based on the Post-Assertion We partition computing Dn into computing Un and Vn, each of that has the same structure with Dn. UBBPermAn ':1 :iinBn In Equation (8), Un denotes the err::1:jjnBjA j (8) number of n elements’  :1AiBiAn or permutation scheme in which an must be the ith element in new permutation B. :VBBPermAj :1:jnBjA j (9)e number of n elements’ n ':1 :iinBn In Equation (9), Vn denotes therr :1AiBiAn  or permutation scheme in which an cannot be the ith element in new permutation B. ::1:DBB PermAj j nBjAj n':1 :iinBn = {Range Disjunction} :1Ai :BBPermA:1:jnBjA j j ':1 :iinBn  :1AiBiAn 1:jnBjA j::BBPermAj ':1 :iinBn = {According to the definition ofAccording to the equation (1puting Dn into computing Un and  :1AiBiAn  Un and Vn } (10) Vn. 3.n-1 elements’ er-ber of n-2 UVnn 0), we can partition com-3 Construct the Recurrence Relation Suppose Dn-1 denotes the number of ror permutation scheme, Dn-2 denotes the numelements’ error permutation scheme. ::1:UBBPermAjjnBjAjn    ':1 ::1iinBnAiBiAn  = {Generalized Range Disjunction}  :1: ::1iinBBPermAjjn [ ]:1An :)[ ][][]BjAjBnAi Bi:1: :iinBBPermA   :1: :1jjiijnBjAj  = {According to the initial definition of D} n :1: )2iinDn (1) 2nDn (11) According to the equation 1), we can partition com-puting Un into computing ( n-1)× Dn-2. (1::1VBBPermAjn :jnBjAj   ':1 :iinBnAiB :1iAn = {Generalized Range Disjunction}  :1: ::1iinBBPermAjjn [ ]:1An :)[ ][][]BjAjBnAiBi:1: :iinBBPermA  :1:[ ][ ] :1jjnBjAj  = {According to the initial definition of Dn } :1: )1iinDn (1) 1nDn (12) According to the equation (12), we can partition com-puting Vn int o computing (n-1) × Dn-1. According to the equation (10)recurrence: D =U + V = (n-1) × (D+D), where Suppose variant s1 stores the value of d(i-2), variant s2 , (11), (12), we have the n nnn-1 n-2D1=0, D2=1. That is to say, we can partition computing Dn into computing (n-1) × D and (n-1n-1 ) × Dn-2. 3.4 Developing Loop Invariant Copyright © 2009 SciRes JSEA Formal Derivation of the Combinatorics Problems with PAR Method Copyright © 2009 SciRes JSEA 199)scheme which are typical combinatorics problems. It is revealed that PAR method has particular merit. It is apt to understand and demonstrate the ingenuity and cor-rectness of an algorithm by formula deduction. Com-pared with other derivation, our algorithmic programs are more precise and simple than the representation of algo-rithm in natural language, flowchart and program. It also shows that using PAR method in developing combina-torics problem is a very natural meaningful research work. This can not only expand the application of PAR method, but also prove that the PAR method is a unified and effective approach on solving combinatorics prob-lems. 5. Acknowledgment stores the value of d(i-1), variant d stores the value of d(i), where D1 =0, D2=1. LI: 1(2)2(1)sdisdi(1 )in (d di 3.5 Developing Corresponding RADL Program Th DL program of the ne RAheme number of error permutation sc, derived by the PAR methods, is show in Algo-rithm 3. By the automatic program transforming system of PAR platform, we can get the APLA program of thenumber of error permutation scheme which is trans-formed from the RADL program and is shown in Algo-rithm 4. Finally, we transform the APLA program of the number of error permutation scheme to C++ program, which can get accurate running result. Algorithm 3 (The RADL program of error permutation scheme) |[in n:integer; i,s1,s2: integer; out d:integer;]| {PQ∧PR} Begin: i=3++1; s1=0; s2=1; A_I: 1221sdisdid di 3in =n+1; Termination: iRecur: d= (i-1)*(s1+s2;s2=d; ); Algorithm The APLA program of error permusc nteger; d:integer; ase input integer n value”); d= (i-1)*(s 1+s2); rrange Scheme:”, z); 4. cWe oped algorithmic programs for the number st the international cooperation ience and Technology of PR  J. Y. Xue, “Aing efficient algorithmic pr computer Science om-orithmic programs [C],” The Proceedings of rmal University, program [J],” Journal of Yunnan University Vo1. 27, rithm with PAR Method [J],” This paper is supported byproject of Ministry of ScChina, grant No. CB 7-2-01, and by Science and Tech-nology research project of Jiangxi Municipal Education Commis sion und er Grant No. GJJ0959 0. REFERENCES unified approach for developograms [J],” Journal ofs1=s2End. 4 (tation puter Sciences and Technology, Vol. 13, No. 6, pp. 95– 102, 1998.  J. Y. Xue, “A practicable approach for formal develop-ment of algand Technology, Vol. 12, No. 4, pp. 103–118, 1997.  J. Y. Xue, “Formal derivation of graph algorithmic pro-grams using Partition-and-Recur [J],” Journal of Cheme) var: n:integer; i:integer; s1,s2: ibegin: te(“Ple The international Symposium on Future software Tech-nology (ISFS'99), Published by Software Engineers As-sociations of Japan, pp. 212–217, 1999.  L. Y. Sun, “The applied research of PAR method on combinatorics problems [D],” Jiangxi No wri read(n); i:=2;s1:=0;s2:=1; do (﹁(i=n)) → 2007.  J. Y. Xue, “Research on formal development of algo-rithmic s1:=s2; s2:=d; i:=i+1; (natural sciences), Vol. 19, pp. 283–288, 1997.  Y. Q. Li, “Partition-and-recur method and its applications [J],” Computer Engineering and Applications, od write(“The Int erlaced Aend. Conlusions develof CNo. 11, pp. 77–79, 2000.  L. Y. Sun and J. Y. Xue, “Formal derivation of the mini-mum spanning tree algoomputer Engineering, Vo1. 32, No. 21, pp. 85–87, 2007. ring scheme and the number of error permutation