A Formal Software Development Approach Using Refinement Calculus  

作　　者：王云峰 庞军 查鸣 杨朝晖 郑国梁 

出　　处：《Journal of Computer Science & Technology》2001年第3期251-262,共12页计算机科学技术学报（英文版）

基　　金：the National Natural Science Foundation of China (No.69673006) and theNational Ninth Five-Year Project (98-780-01-07-06) of Ch

摘　　要：The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calculus into COOZ overcomes its disadvantage during design and implementation. The separation between the design and implementation for structure and notation is removed as well. Then the software can be developed smoothly in the same frame. The combina- tion of COOZ and refinement calculus call build object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In this paper, the development model is established, which is based on COOZ and refinement calculus. Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. As to the implemelltation technology of refinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calculus into COOZ overcomes its disadvantage during design and implementation. The separation between the design and implementation for structure and notation is removed as well. Then the software can be developed smoothly in the same frame. The combina- tion of COOZ and refinement calculus call build object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In this paper, the development model is established, which is based on COOZ and refinement calculus. Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. As to the implemelltation technology of refinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.

关 键 词：formal development method refinement calculus formal specification OBJECT-ORIENTED 

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