Class refinement and interface refinement in object-oriented programs

  • Anna Mikhajlova
  • Emil Sekerinski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


Constructing new classes from existing ones by inheritance or subclassing is a characteristic feature of object-oriented development. Imposing semantic constraints on subclassing allows us to ensure that the behaviour of superclasses is preserved or refined in their subclasses. This paper defines a class refinement relation which captures these semantic constraints. The class refinement relation is based on algorithmic and data refinement supported by Refinement Calculus. Class refinement is generalized to interface refinement, which takes place when a change in user requirements causes interface changes of classes designed as refinements of other classes. We formalize the interface refinement relation and present rules for refinement of clients of the classes involved in this relation.


Object Type Proof Obligation Data Refinement Class Account Interface Change 
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.
    M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.Google Scholar
  2. 2.
    M. Abadi and K. R. M. Leino. A logic of object-oriented programs. In Theory and Practice of Software Development: Proceedings / TAPSOFT '97, volume LNCS 1214, pages 682–696. Springer, April 1997.Google Scholar
  3. 3.
    P. America. Designing an object-oriented programming language with behavioral subtyping. In J.W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, REX School/Workshop, volume LNCS 489, pages 60–90, New York, N.Y., 1991. Springer-Verlag.Google Scholar
  4. 4.
    R. J. R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980.Google Scholar
  5. 5.
    R. J. R. Back. Changing data representation in the refinement calculus. In 21st Hawaii International Conference on System Sciences. IEEE, January 1989.Google Scholar
  6. 6.
    R. J. R. Back and J. von Wright. Refinement calculus I: Sequential nondeterministic programs. In W. P. deRoever J. W. deBakker and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, pages 42–66. Springer-Verlag, 1990.Google Scholar
  7. 7.
    R.J.R. Back and M.J. Butler. Exploring summation and product operators in the refinement calculus. In B. Möller, editor, Mathematics of Program Construction, 1995, volume LNCS 947. Springer-Verlag, 1995.Google Scholar
  8. 8.
    M. Broy. (Inter-)Action Refinement: The Easy Way. In M. Broy, editor, Program Design Calculi, pages 121–158, Berlin Heidelberg, 1993. Springer-Verlag.Google Scholar
  9. 9.
    L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471–522, 1985.CrossRefGoogle Scholar
  10. 10.
    K. K. Dhara and G. T. Leavens. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 19th International Conference on Software Engineering, pages 258–267, Berlin, Germany, 1996.Google Scholar
  11. 11.
    E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Professional Computing Series. Addison-Wesley, 1995.Google Scholar
  12. 12.
    P.H. Gardiner and C.C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87(1):143–162, 1991.Google Scholar
  13. 13.
    J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Sun Microsystems, Mountain View, 1996.Google Scholar
  14. 14.
    J. He, C. A. R. Hoare, and J. W. Sanders. Data refinement refined. In B. Robinet and R. Wilhelm, editors, European Symposium on Programming, volume LNCS 213. Springer-Verlag, 1986.Google Scholar
  15. 15.
    C. A. R. Hoare. Proofs of correctness of data representation. Acta Informatica, 1(4):271–281, 1972.CrossRefGoogle Scholar
  16. 16.
    K. Lano and H. Haughton. Reasoning and refinement in object-oriented specification languages. In O. Lehrmann Madsen, editor, European Conference on Object-Oriented Programming '92, volume LNCS 615. Springer-Verlag, 1992.Google Scholar
  17. 17.
    K. Lano and H. Haughton. Object-Oriented Specification Case Studies. PrenticeHall, New York, 1994.Google Scholar
  18. 18.
    B. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811–1841, 1994.Google Scholar
  19. 19.
    C. C. Morgan. Data refinement by miracles. Information Processing Letters, 26:243–246, 1988.MathSciNetGoogle Scholar
  20. 20.
    C. C. Morgan. Programming from Specifications. Prentice-Hall, 1990.Google Scholar
  21. 21.
    J. M.Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.CrossRefGoogle Scholar
  22. 22.
    D. A. Naumann. Predicate transformer semantics of an Oberon-like language. In Ernst-R. Olderog, editor, Programming Concepts, Methods and Calculi, pages 460–480. International Federation for Information Processing, 1994.Google Scholar
  23. 23.
    J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-Oriented Modelling and Design. Prentice Hall, Englewood Cliffs, 1991.Google Scholar
  24. 24.
    E. Sekerinski. Verfeinerung in der Objektorientierten Programmkonstruktion. Dissertation, Universität Karlsruhe, 1994.Google Scholar
  25. 25.
    E. Sekerinski. A type-theoretic basis for an object-oriented refinement calculus. In S.J. Goldsack and S.J.H. Kent, editors, Formal Methods and Object Technology. Springer-Verlag, 1996.Google Scholar
  26. 26.
    C. A. Szyperski, S. Omohundro, and S. Murer. Engineering a programming language — the type and class system of Sather. In Proceedings, First Intl Conference on Programming Languages and System Architectures, volume LNCS 782, Zurich, Switzerland, 1994. Springer.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Anna Mikhajlova
    • 1
  • Emil Sekerinski
    • 2
  1. 1.Turku Centre for Computer ScienceÅbo Akademi UniversityTurkuFinland
  2. 2.Dept. of Computer ScienceÅbo Akademi UniversityTurkuFinland

Personalised recommendations