A Formal Software Development Approach Using Refinement Calculus

The advantage of COOZ (Complete Object-Oriented Z)is to specify large scalesoftware, but it does not support refinement calculus. Thus itsapplication is confined %and it cannot be taken as a whole methodforsoftware development. Including refinement calculus into COOZovercomes its disadvantage during design and implementation. Theseparation between the design and implementation for structure and notationis removed as well. Then the software can be developed smoothly in thesame frame. The combination of COOZ and refinement calculus can buildobject-oriented frame, in which the specification in COOZ is refinedstepwise to code by calculus. In this paper, the development model isestablished, which is based on COOZ and refinement calculus. Datarefinement is harder to deal with in a refinement tool than ordinaryalgorithmic refinement, since data refinement usually has to be done ona large program component at once. As to the implementation technology ofrefinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on datarefinement calculus and program window inference is offered.