The Research And Application Of B Language And Method In Algorithm Formalization

B-Method is a strict method to describe and design computer software. Its function extends to code generation, and it uses pseudo programming to describe module requirement and to design and implement software. B is established on Zermelo-Frankel set theory. It expresses states transferring by signal method. So both program and its specification are on uniform framework, which can reduce the possibility of semantic error. With the support of BToolkit, this formalized B-method improves software reliability and Automation efficiency greatly.Algorithm formalization is concentrated on how to describe the algorithm by fomalize method,how to construct an implementation of an algorithm by formalize deriving. We can combine the algorithm deriving process with the proving process by using B-Method and B-Tool set.The proof technology that B-method uses will simplify and automatize the process of algorithm construction proving.The theory of refinement and the research of automatic refiner will make great effect in automatic construction of algorithm.This paper focuses on how to describe the algorithm using B-Method, how to construct an algorithm implementation according to the description of algorithm with B-Method.We will propose some advisable resolutions to this matter.Then we practice some examples in the integrated environment of BToolkit,and also introduce basic develop process under BToolkit environment. In the end,we give some advice about further research in this aspect.