摘要： 形式化方法B支持从抽象规约到实现的完整的开发过程，用于开发安全关键的软件系统。给出了B方法精化的定义后，介绍了抽象机的精化过程与方法，结合实例分析了仅使用前向精化的普通精化规则的不完整性，通过引入反向精化提供了完备的精化理论，二者联合起来能够证明任何正确的精化。

关键词: 形式化方法, 广义代换, 抽象机, 前向精化, 反向精化, 证明义务

Abstract: Formal method B supports the whole development from abstract specifications to implementation, which is used to develop safety-critical systems in software. This paper presents the definition of refinement in B and describes the refinement process of abstract machine and its approaches. After illuminating via an example that B’s ordinary refinement rules only in terms of forward refinement are incomplete, backward refinement is introduced to endow B for the first time with two tractable and jointly complete refinement theories which together are sufficient for proving any valid refinement.

Key words: Formal method, Generalized substitution, Abstract machine, Forward refinement, Backward refinement, Proof obligations