Borba, P.H.M. and Sampaio, A.C.A. and Cavalcanti, A.L.C. and Cornelio, M.L. (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 available from this repository. (Contact us about this Publication) | |
| Official URL http://dx.doi.org/10.1016/j.scico.2004.03.003 |
Abstract
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: | 13 Jul 2009 00:31 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/14221 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
