形式化软件功能分解的交互式规则

Interactive Rules of Formal Software Function Decomposition

形式化功能分解是软件形式化设计的基本手段。文章基于前后断言形式定义的软件功能，提出了一组将该功能定义分解为3种基本控制结构之一的交互式分解规则，并证明了这组分解规则的正确性。分解规则构成的规则库是支持软件形式化设计的知识库的重要组成部分。

Formal function decomposition is the essential method of formal softWare design. In this paper,based on the formal software functions defined hy precondition and postcondition,we propose a guup of interactive rules which can decompose a function into one of the basic contrnl structures and prove the correctness of these rules. The rule base composed of these rules is an important part of knowledge hase supporting formal software design.