%0 Journal Article %1 borba_04_algebraic %A Borba, Paulo %A Sampaio, Augusto %A Cavalcanti, Ana %A Corn'elio, M'arcio %B Special Issue on Program Transformation %D 2004 %J Science of Computer Programming %K 2004 %N 1-3 %P 53--100 %R 10.1016/j.scico.2004.03.003 %T Algebraic reasoning for object-oriented programming %U http://dx.doi.org/10.1016/j.scico.2004.03.003 %V 52 %X 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.

@article{borba_04_algebraic, 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.}, added-at = {2009-02-11T21:04:59.000+0100}, author = {Borba, Paulo and Sampaio, Augusto and Cavalcanti, Ana and Corn'{e}lio, M'{a}rcio}, biburl = {https://www.bibsonomy.org/bibtex/232662283d60659bda56e542c0e2197bf/leonardo}, booktitle = {Special Issue on Program Transformation}, citeulike-article-id = {1725027}, doi = {10.1016/j.scico.2004.03.003}, interhash = {85af54a15d48e3cdad64b0cc80d828c9}, intrahash = {32662283d60659bda56e542c0e2197bf}, journal = {Science of Computer Programming}, keywords = {2004}, month = {August}, number = {1-3}, pages = {53--100}, posted-at = {2008-02-25 14:49:43}, priority = {2}, timestamp = {2009-02-11T21:04:59.000+0100}, title = {Algebraic reasoning for object-oriented programming}, url = {http://dx.doi.org/10.1016/j.scico.2004.03.003}, volume = 52, year = 2004 }