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)|
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:||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):