The Applied Research Of PAR Method On Combinatorics Problems

Computer science is a science of studying algorithms, while algorithms in computer are mostly used to handling discrete objects. It is the combinatorial algorithms which based on a science of studying discrete objects, Combinatorics, that make people feel that computer may have its own thought. However, many teaching material about combinatorial algorithms can only produce algorithms but can't provide the designing process from unresolved problem to exact algorithmic programs, which seriously impair understanding ingenious thought of algorithms and hold back the improvement of algorithms designing.Prof. Xue Jinyun addresses and solves a series of critical techniques and forms the PAR method and its supporting platform supported by several national and provincial research projects. The actual project is the Nation's Natural Science Fund Project "the research of designing algorithm formally and automatically based on PAR method". It involves two aspects: developing software formally and automatically, deriving and testifying algorithmic program formally. In this thesis, we formally derive Combinatorics problems by PAR method, which can not only solve those above problems, but also can assure their correctness on logic. PAR method embodies rich mathematic ideology and is provided with many powerful tools and appropriate developing environment. Therefore, through adopting it on developing Combinatorics algorithms, we can avoid making a choice among various designing methods. It can also change many creative labors to mechanized labors, and can finally improve algorithmic programs design's automatization and standardization.The following are the main research works in this thesis: Analyze current formalization requirement, introduce several typical formal methods for software development and study Specware, a software developing system, which is invented by the academic group led by Prof. Smith. Introduce the critical techniques, developing process and language of PAR method and compare it with typical formal methods and Specware. Analyze characteristic of PAR method and demonstrate its effectiveness on Combinatorics problems. Finally, develop several typical algorithms of Combinatorics problem instances such as: String Scheme Number, Interlaced Arrange Scheme Number, Maximum Summary, the Longest Common Subsequence, Minimum Spanning Tree and the Knapsack Problem, etc. Analyze and summarize its developing steps.In this thesis, we make creative novelties in many aspects. Study the basal theory, developing process and principle of Specware and compare it with PAR method. Address that PAR method is really an effective formal method on solving Combinatorics problems. Apply its generic system on developing process. Use PAR method on Combinatorics problem instances to lay out the deriving process from specifications to algorithms and study its practicability which based on the institution from the whole process for the first time.