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 Borba | 1 | 1088 | 68.71 |
Augusto Sampaio | 2 | 85 | 4.06 |
Ana Cavalcanti | 3 | 224 | 18.41 |
Márcio Cornélio | 4 | 123 | 9.43 |