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

Machine-aided Refinement Techniques of Formal Specification

作　　者：袁晓东[1] 郑国梁[2] 

机构地区：[1]电力部电力自动化研究院仿真室,南京210003 [2]南京大学计算机软件新技术国家重点实验室,计算机科学与技术系南京210093

出　　处：《计算机科学》1998年第6期19-23,共5页Computer Science

基　　金：国家九五攻关项目;国家自然科学基金

摘　　要：形式化规格说明为我们提供一个简洁、精确且能被很好理解的系统描述。但我们还需要从规格说明得到其合适的代码实现,这一开发过程称为形式化规格说明的求精[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++.

关 键 词：形式化规格说明 机器辅助 求精技术 形式语言 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]