Formal Derivation of the Interlaced Arrange Scheme Number Combinatorics Problem with PAR Method
Lingyu Sun, Ming Leng · 2009
Partition-and-Recur (PAR) method is a simple and useful formal method used to design and prove algorithmic programs. In this paper, we address thatPARmethod is really an effective formal method on solving Combinatorics problems. We formally derive Combinatorics problems byPARmethod, which cannot 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, interlaced arrange scheme number, and get accurate running result by RADL algorithmic program which derived byPARmethod and can be transformed to C++ programs by the automatic program transforming system ofPARplatform.