This thesis is a step towards a programming method which supports a calculational style and is useful for the production of large software systems.
Object orientation is a popular programming paradigm for the development of large-scale systems. It is based on the idea that software should be a set of communicating entities, of which many entities are models of real objects.
The refinement calculus is a notation and set of rules that supports a calculational approach to the formal development of software. It is envisaged that when the object-oriented paradigm and refinement calculus are fused, the resulting method would provide a development path for large-scale, provably correct software.
Several attempts have been made to construct an object-oriented refinement calculus. This thesis discusses several of these and summarises the remainder. The approaches include the modular
reasoning work of Utting and Robinson |UR92|, the type theoretic approaches of Mikhajlova and Sekerinski [MS97] and the higher-order approach of Cavalcanti and Naumann |CN99].
The thesis utilises a typed object calculus as the infrastructure of an alternative approach to the development of an object-oriented refinement calculus. Object calculi are a notation and set of rules that are used to model the concepts of object orientation. They have been used as the basis of several object-oriented languages.
Both a semantics of object values and a semantics of references for an object-oriented refinement calculus are presented within the thesis. Additionally, both object-based and class-based object-oriented refinement calculi are supported.
The development of programs that contain references can be tedious. A novel development method, termed coalescing, is introduced to allow unnecessary aliasing to be temporarily
removed. Another novel technique is introduced to allow the development of reference semantics programs using a simpler value semantics.
Examples are presented which illustrate the capabilities of program development using an object-oriented refinement calculus. One example presents the application of the iterative, incremental development process of the object-oriented paradigm within the refinement calculus.