The Research And Application Of Loop Invariant Development Strategy For Two Kinds Of Combinatorial Mathematical Problems

With the increasing popularity of computer applications,the accuracy and reliability of computer software are highly valued in various fields,especially in some key fields such as market economy,traffic safety,aerospace and so on,which are of vital importance.Algorithm is the core of software,which plays an important role in software development,formal method is one of the effective ways to ensure the correctness and reliability of the algorithm.Loop invariant plays a very important role in algorithmic formalization,it is the key to understand,develop and prove an algorithmic program.Loop invariant development has been one of the most challenging and creative issues in the formalized world,there are many difficulties in finding a loop invariant development strategy.Combinatorial mathematics is a branch of mathematics that develops rapidly after the appearance of computers,its theoretical advancement also promotes the rapid development of computer science,in the field of computer science,the algorithm solution of many problems is based on combinatorial mathematics,therefore,the algorithm research of combinatorial mathematical problems has become an important research field in computer science.In combinatorial mathematics,sequence problem and permutation and combination problem are the two most classical and representative problems,therefore,this paper focuses on the loop invariant development technology of sequence and permutation algorithms.In this paper,the role of loop invariants in the formalization of algorithms is further explored,and the existing loop invariants development techniques and strategies are analyzed and compared.Secondly,through the in-depth study of the Catalan and Fibonacci sequence problems in combinatorial mathematics,and according to the mathematical properties and solving characteristics of these two sequence problems,a loop invariant development strategy for sequence problems is proposed.At the same time,based on the in-depth analysis of the solving process of the permutation problem in combinatorial mathematics,based on the decomposition of the solved problem,by describing the properties of the processed and unprocessed parts and the relationship between them,the invariant properties in the problemsolving process are extracted,and two specific development strategies of permutation problem's loop invariant are proposed,thus it provides an effective way to develop loop invariants for two kinds of combinatorial mathematical problems.In this paper,the proposed loop invariant development strategy is applied to the development of loop invariant for some sequence problems and permutation problems,and the formal derivation process of algorithm programs for these problems is completed based on the developed loop invariant.Thus,while obtaining the algorithms for solving these problems,it also effectively guarantees the correctness of these algorithms.