The Implementation And Application Of B-Method In Abstract Machine Library

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 B-toolkit, this formalized B-method improves software reliability and Automation efficiency greatly.At present, B-Methods have been applied to a wide range of technical areas successfully in overseas, including real-time, simulation, information processing and engineering, especially Paris tube-train signaling system, which contribute to decrease train spacing and improve security of the whole iron system. But the study on B-Method is just the first step at home. So, this paper concentrates on the use of B-Method in programming.Firstly, this paper focuses on designing an abstract machine library, which uses the specification statement to build machine model that can complete some basic mathematical computation; Secondly, the idea of elementary refinement is presented here, which implements a transformation from abstracting program to concreting program by the transform of data or function; Then using mathematical principle, especially Dijkstra's weakest preconditions theory, to complete proof of specification and refinement. Dijkstra's theory combines alternating of program development with correctness proof to programming. It improves the accuracy and reduces the cycle of programming. On this basis, automatic refinement algorithm is introduced to complete data generation of machine and it can gradually refine the abstract specification to a performable procedure. The program correctness depends on the validity of each step in refinement process; Finally, implementation is completed by using distributed theory.This paper primly introduces the validation and feasibility of B-Method at abstract machine library in practice, aiming at providing certain reference and significance in this filed, and hoping further and wide research can be done in the future in China.