Algebraic Reasoning for Object-Oriented Programming

Borba, Paulo H.M. and Sampaio, Augusto C.A. and Cavalcanti, Ana L. C. and Cornélioa, Márcio (2004) Algebraic Reasoning for Object-Oriented Programming. Science of Computer Programming, 52 (1-3). pp. 53-100. ISSN 0167-6423 . (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL


We present algebraic laws for a language similar to a subset of sequential Java that includes inheritance, recursive classes, dynamic binding, access control, type tests and casts, assignment, but no sharing. These laws are proved sound with respect to a weakest precondition semantics. We also show that they are complete in the sense that they are sufficient to reduce an arbitrary program to a normal form substantially close to an imperative program; the remaining object-oriented constructs could be further eliminated if our language had recursive records. This suggests that our laws are expressive enough to formally derive behaviour preserving program transformations; we illustrate that through the derivation of provably-correct refactorings.

Item Type: Article
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:02
Last Modified: 12 Jun 2014 08:39
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):