From Object-Oriented Z Specification to Code by Refinement Calculus

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 and it can not be taken as a complete method for software development. Including refinement calculus into COOZ remedies 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. In this paper, development model is established, which is based on COOZ and refinement calculus. Data refinement and operation refinement are debated with a example. As for implementary technology of refinement calculus, a data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is provided.