A Refinement Algebra for Object-Oriented Programming

  • Paulo Borba
  • Augusto Sampaio
  • Márcio Cornélio
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2743)


In this article we introduce a comprehensive set of algebraic laws for ROOL, a language similar to sequential Java but with a copy semantics. We present a few laws of commands, but focus on the object-oriented features of the language. We show that this set of laws is complete in the sense that it is sufficient to reduce an arbitrary ROOL program to a normal form expressed in a restricted subset of the ROOL operators. We also propose a law for data refinement that generalises the technique from traditional modules to class hierarchies. Together, these laws are expressive enough to derive more elaborate rules that can be useful, for example, to formalize object-oriented design practices; this is illustrated through the systematic derivation of a refactoring from the proposed laws.


Normal Form Object Class Method Call Class Hierarchy Private Attribute 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Hoare, C.A.R., et al.: Laws of programming. Communications of the ACM 30, 672–686 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)zbMATHGoogle Scholar
  3. 3.
    Sampaio, A.: An Algebraic Approach to Compiler Design. Algebraic Methodology and Software Technology, vol. 4. World Scientific, Singapore (1997)zbMATHCrossRefGoogle Scholar
  4. 4.
    Roscoe, A., Hoare, C.A.R.: The laws of occam programming. Theoretical Computer Science 60, 177–229 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall, Englewood Cliffs (1997)zbMATHGoogle Scholar
  6. 6.
    Seres, S., Spivey, M., Hoare, T.: Algebra of logic programming. In: ICPL 1999, New Mexico, USA (1999) Google Scholar
  7. 7.
    Hoare, C., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  8. 8.
    Fowler, M.: Refactoring—Improving the design of existing code. Addison-Wesley, Reading (1999)Google Scholar
  9. 9.
    Lea, D.: Concurrent Programming in Java. Addison-Wesley, Reading (1997)zbMATHGoogle Scholar
  10. 10.
    Opdyke, W.: Refactoring Object-Oriented Frameworks. PhD thesis, University of Illinois at Urbana-Champaign (1992) Google Scholar
  11. 11.
    Roberts, D.: Practical Analysis for Refactoring. PhD thesis, University of Illinois at Urbana Champaign (1999) Google Scholar
  12. 12.
    Mikhajlova, A., Sekerinsk, E.: Class refinement and interface refinement in object-oriented programs. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 82–101. Springer, Heidelberg (1997)Google Scholar
  13. 13.
    Leino, K.R.M.: Recursive Object Types in a Logic of Object-oriented Programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, p. 170. Springer, Heidelberg (1998)Google Scholar
  14. 14.
    Evans, A.: Reasoning with UML class diagrams. In: Workshop on Industrial Strength Formal Methods, WIFT 1998, Florida, USA. IEEE Press, Los Alamitos (1998)Google Scholar
  15. 15.
    Evans, A., France, R., Lano, K., Rumpe, B.: The UML as a formal modeling notation. In: Bézivin, J., Muller, P.-A. (eds.) UML 1998. LNCS, vol. 1618, pp. 336–348. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. 16.
    Lano, K., Bicarregui, J.: Semantics and transformations for UML models. In: Bézivin, J., Muller, P.-A. (eds.) UML 1998. LNCS, vol. 1618, pp. 107–119. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  17. 17.
    Gogolla, M., Richters, M.: Transformation rules for UML class diagrams. In: Bézivin, J., Muller, P.-A. (eds.) UML 1998. LNCS, vol. 1618, pp. 92–106. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  18. 18.
    Booch, G., Jacobson, I., Rumbaugh, J.: The Unified Modelling Language User Guide. Addison-Wesley, Reading (1999)Google Scholar
  19. 19.
    Cavalcanti, A., Naumann, D.: A weakest precondition semantics for an objectoriented language of refinement. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1439–1459. Springer, Heidelberg (1999)Google Scholar
  20. 20.
    Cavalcanti, A., Naumann, D.: A weakest precondition semantics for refinement of object-oriented programs. IEEE Transactions on Software Enginnering 26, 713–728 (2000)CrossRefGoogle Scholar
  21. 21.
    Arnold, K., Gosling, J.: The Java Programming Language. Addison Wesley, Reading (1996)zbMATHGoogle Scholar
  22. 22.
    Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)zbMATHGoogle Scholar
  23. 23.
    Cornélio, M. L.: Applying Object-oriented Refactoring and Patterns as Formal Refinements. PhD thesis, Informatics Center, Federal University of Pernambuco, Brazil (to appear in 2003) Google Scholar
  24. 24.
    Lira, B.O.: Automação de Regras para Programação Orientada a Objetos. Master’s thesis, Centro de Informática, Universidade Federal de Pernambuco, Brazil (2002) Google Scholar
  25. 25.
    Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Object-Oriented Programming, pp. 314–390. MIT Press, Cambridge (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Paulo Borba
    • 1
  • Augusto Sampaio
    • 1
  • Márcio Cornélio
    • 1
  1. 1.Informatics CenterFederal University of PernambucoRecifeBrazil

Personalised recommendations