Towards an object-oriented refinement calculus

Shield, Jamie Barry Nathan. (2004). Towards an object-oriented refinement calculus PhD Thesis, School of Information Technology and Electrical Engineering, The University of Queensland.

       
Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
THE17862.pdf Full text application/pdf 10.25MB 2
Author Shield, Jamie Barry Nathan.
Thesis Title Towards an object-oriented refinement calculus
School, Centre or Institute School of Information Technology and Electrical Engineering
Institution The University of Queensland
Publication date 2004
Thesis type PhD Thesis
Supervisor Carrington, D.
Total pages 272
Collection year 2004
Language eng
Subjects L
280302 Software Engineering
700199 Computer software and services not elsewhere classified
Formatted abstract 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.
Keyword Computer programming

 
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 71 Abstract Views, 2 File Downloads  -  Detailed Statistics
Created: Fri, 24 Aug 2007, 18:25:28 EST