Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
1999 Technical Reports

An Object-Oriented Refinement Calculus

Richard F. Paige and Jonathan S. Ostroff

Technical Report CS-1999-07

York University

December 21, 1999


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.