J. Software Engineering & Applications, 2009, 2: 195-199
doi:10.4236/jsea.2009.23026 Published Online October 2009 (http://www.SciRP.org/journal/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.
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



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


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

Formal Derivation of the Combinatorics Problems with PAR Method 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