Formal Derivation of the Longest Common Subsequence Problem with PAR Method

Partition-and-Recur (PAR) method is a simple and useful formal method used to design and prove algorithmic programs. In this paper, we address that PAR method is really an effective formal method on solving Combinatorics problems. We formally derive Combinatorics problems by PAR method, which can not only simplify the process of algorithmic program´s designing and correctness testifying, but also effectively improve the automatization, standardization and correctness of algorithmic program´s designing by changing many creative labors to mechanized labors. Lastly, we develop typical algorithms of Combinatorics problem instances, longest common subsequence problem, and get accurate running result by RADL algorithmic program which derived by PAR method and can be transformed to C++ programs by the automatic program transforming system of PAR platform.