Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.
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.
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.
R. J. R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980.
R. J. R. Back. Changing data representation in the refinement calculus. In 21st Hawaii International Conference on System Sciences. IEEE, January 1989.
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.
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.
M. Broy. (Inter-)Action Refinement: The Easy Way. In M. Broy, editor, Program Design Calculi, pages 121–158, Berlin Heidelberg, 1993. Springer-Verlag.
L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471–522, 1985.
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.
E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Professional Computing Series. Addison-Wesley, 1995.
P.H. Gardiner and C.C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87(1):143–162, 1991.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Sun Microsystems, Mountain View, 1996.
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.
C. A. R. Hoare. Proofs of correctness of data representation. Acta Informatica, 1(4):271–281, 1972.
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.
K. Lano and H. Haughton. Object-Oriented Specification Case Studies. PrenticeHall, New York, 1994.
B. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811–1841, 1994.
C. C. Morgan. Data refinement by miracles. Information Processing Letters, 26:243–246, 1988.
C. C. Morgan. Programming from Specifications. Prentice-Hall, 1990.
J. M.Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.
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.
J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-Oriented Modelling and Design. Prentice Hall, Englewood Cliffs, 1991.
E. Sekerinski. Verfeinerung in der Objektorientierten Programmkonstruktion. Dissertation, Universität Karlsruhe, 1994.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mikhajlova, A., Sekerinski, E. (1997). Class refinement and interface refinement in object-oriented programs. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_5
Download citation
DOI: https://doi.org/10.1007/3-540-63533-5_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63533-8
Online ISBN: 978-3-540-69593-6
eBook Packages: Springer Book Archive