An Object-Oriented Refinement Calculus
Richard F. Paige and Jonathan S. Ostroff
Technical Report CS-1999-07
York University
December 21, 1999
Abstract
Design-by-contract has been used in the BON/Eiffel setting as an industrial-strength technique for building reliable, reusable, and maintainable software systems. We show that it also provides a basis for carrying out the refinement of object-oriented specifications to programs on an industrial scale. We present a collection of algorithm refinement rules, in particular, novel rules for introducing feature calls which is the basis of object-oriented computing, as well as a new loop rule for a double-state loop invariant. We show how refinement of large systems can be decomposed into many small steps. And we describe how automated support for such a process can be developed.
(Revised August 2000. Further revisions pending.)
Download paper in PDF format.
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.