Title
Algebraic reasoning for object-oriented programming
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.
Year
DOI
Venue
2004
10.1016/j.scico.2004.03.003
Sci. Comput. Program.
Keywords
Field
DocType
recursive record,algebraic law,access control,imperative program,object-oriented programming,provably-correct refactorings,program transformation,recursive class,normal form,derive behaviour,arbitrary program,algebraic reasoning,dynamic binding,computer programming,object oriented programming,object oriented,weakest precondition
Predicate transformer semantics,Algebraic number,Programming language,Object-oriented programming,Computer science,Theoretical computer science,A-normal form,Java,Semantics,Computer programming,Recursion
Journal
Volume
Issue
ISSN
52
1-3
Science of Computer Programming
Citations 
PageRank 
References 
46
1.83
25
Authors
4
Name
Order
Citations
PageRank
Paulo Borba1108868.71
Augusto Sampaio2854.06
Ana Cavalcanti322418.41
Márcio Cornélio41239.43