### Paper Menu >>

### Journal Menu >>

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 195 Formal 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 [4]. 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 [4], the longest common subsequence [4], minimum spanning tree [4,7] and the Knapsack problem [4], 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? [4] 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 ,: F Sij ij 1ba , then :..1nSjjab Sj ..j (: (): Z NSSString n n (:1:[1][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 X n and Yn , each of that has the same structure with Zn. (:() (,1) X SSString nFS n ([1][1] ):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 S n ([1][1] ):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 S n (:() (,1)SSString nFS ([1][1][1][1]) :1)SaSbScSd ={Range Disjunction} ( :()(,1) ([1][1]):1)SSStringnF SSaSb (:()(,1)([1][1]) :1)SSString nFSScSd = {According to the definition of Xn and Yn} X Y nn (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) X SSStringnFS n ([1][1] ):1)SaSb ( :()(,1) ([1]SSString nF SS [1])([2]aSbS [2][2][2]):1)aS bS cSd = {Range Disjunction} (:( )(,1)([1][2])SSString nFSSS ([2][2] ):1)SaSb (:( )(,1)([1])SSString nF SSa ([2][2]):1)ScSd (:( )(,1)([1])SSString nF SSb ([2][2]):1)ScSd = {According to the definition of } ,FSi (:() ([1][2])(,2)SS StringnSSFS ([2][2] ):1)SaSb (:() ([1])(,2)SSString nSaFS ([2][2]):1)ScSd (:() ([1])(,2)SSString nSbFS ([2][2]):1)ScSd = {According to the definition of Xn-1 and Yn-1 } 2 1 XY n 1n (5) According to the equation (5), we can partition com- puting Xn into computing Xn-1 and 2×Yn-1. (:() (,1)YSSString nFS n ([1][1] ):1)ScSd ( :()(,1) ([1]SSString nF SS [1])( [2][2]cSd SaS [2][2] ):1)bS cS d Copyright © 2009 SciRes JSEA Formal Derivation of the Combinatorics Problems with PAR Method 197 = {Range Disjunction} (:( )(,1)([1][2])SSString nF SScSd ([2][2] ):1)SaSb (:( )(,1)([1][2])SSString nF SScSd ([2][2]):1)ScSd = {Range Disjunction} (:( )(,1)( [1])SSString nFSSc ([2][2] ):1)SaSb (:( )(,1)( [1])SS StringnFSSd ([2][2] ):1)SaSb (:( )(,1)( [1])SSString nF SSc ([2][2]):1)ScSd (:( )(,1)( [1])SS StringnFSSd ([2][2]):1)ScSd = {According to the definition of , F Si } (:() ([1])(,2)SS StringnScFS ([2][2] ):1)SaSb 1n (:() ([1])(,2)SSString nSdF S ([2][2] ):1)SaSb (:() ([1])(,2)SS StringnScFS ([2][2]):1)ScSd (:() ([1])(,2)SSString nSdF S ([2][2]):1)ScSd = {According to the definition of Xn-1 and Yn-1 } 22 1 XY n (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: 11 x XuXyYvYzZ ii ii (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 x xiuxiyyi 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? [4] 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 ABB 1,, }ij k nj k . PR: Let [][] [][]jA iBjBk , then ::1: D NBB PermA n 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. UBBPermA n ':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 th err :1AiBiAn or permutation scheme in which an cannot be the ith element in new permutation B. ::1: D BB 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 of According to the equation (1 puting Dn into computing Un and :1AiBiAn Un and Vn } (10) Vn. 3. n-1 elements’ er- ber of n-2 UV nn 0), we can partition com- 3 Construct the Recurrence Relation Suppose Dn-1 denotes the number of ror permutation scheme, Dn-2 denotes the num elements’ error permutation scheme. ::1:UBBPermAjjnBjAj n ':1 ::1iinBnAiBiAn = {Generalized Range Disjunction} :1: ::1iinBBPermAjjn [ ]:1An :)[ ][][]BjAjBnAi Bi :1: :iinBBPermA :1: :1jjiijnBjAj = {According to the initial definition of D} n :1: ) 2 iinD n (1) 2 nD n (11) According to the equation 1), we can partition com- puting Un into computing ( n-1)× Dn-2. (1 ::1VBBPermAj n :jnBjAj ':1 :iinBnAiB :1iAn = {Generalized Range Disjunction} :1: ::1iinBBPermAjjn [ ]:1An :)[ ][][]BjAjBnAiBi :1: :iinBBPermA :1:[ ][ ] :1jjnBjAj = {According to the initial definition of Dn } :1: ) 1 iinD n (1) 1 nD n (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-2 D1=0, D2=1. That is to say, we can partition computing Dn into computing (n-1) × D and (n-1 n-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) s disdi (1 )in (d di 3.5 Developing Corresponding RADL Program Th DL program of the ne RA heme n umber 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 the number 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: 1221 s disdid di 3in =n+1; Termination: i Recur: d= (i-1)*(s1+s2 ;s2=d; ); Algorithm The APLA program of error permu sc nteger; d:integer; ase input integer n value”); d= (i-1)*(s 1+s2); rrange Scheme:”, z); 4. c We oped algorithmic programs for the number st the international cooperation ience and Technology of PR [1] 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 by project of Ministry of Sc China, 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 develop ograms [J],” Journal of s1=s2 End. 4 (tation puter Sciences and Technology, Vol. 13, No. 6, pp. 95– 102, 1998. [3] J. Y. Xue, “A practicable approach for formal develop- ment of alg and Technology, Vol. 12, No. 4, pp. 103–118, 1997. [2] J. Y. Xue, “Formal derivation of graph algorithmic pro- grams using Partition-and-Recur [J],” Journal of C heme) var: n:integer; i:integer; s1,s2: i begin: te(“Ple The international Symposium on Future software Tech- nology (ISFS'99), Published by Software Engineers As- sociations of Japan, pp. 212–217, 1999. [4] 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. [5] 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. [6] Y. Q. Li, “Partition-and-recur method and its applications [J],” Computer Engineering and Applications, od write(“The Int erlaced A end. Conlusions develof C No. 11, pp. 77–79, 2000. [7] L. Y. Sun and J. Y. Xue, “Formal derivation of the mini- mum spanning tree algo omputer Engineering, Vo1. 32, No. 21, pp. 85–87, 2007. ring scheme and the number of error permutation |