机器辅助下的形式化规格说明求精技术

Machine-aided Refinement Techniques of Formal Specification

形式化规格说明为我们提供一个简洁、精确且能被很好理解的系统描述。但我们还需要从规格说明得到其合适的代码实现,这一开发过程称为形式化规格说明的求精[lj。规格说明的求精技术已经有比较深入的研究,一般要通过数据求精和操作求精逐步精化的过程,逐步降低抽象级,最终得到规格说明的程序实现代码。但现有的精化理论较少考虑机器辅助技术的应用。

Presently the refinement from formal specifications to program codes is mainly completed by manual work with little automatic techniques. To adopt machine-aided techniques in the process of refinement as more as possible, this paper introduces a new refinement steps from formal specifications written in an object-oriented extension to Z named COOZ to C++ program, and describes the strategies and steps of operation refinement such as automatic generation of program frame, stepped implementation of specification sentence and predicate transition in detail. This paper also introduces data refinement rules from abstract types of COOZ to concrete types of C++ , and illustrates how to implement various abstract mathematical operators using code library written in templates of C++.