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)
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.
|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:||https://kar.kent.ac.uk/id/eprint/14221 (The current URI for this page, for reference purposes)|