Where academic tradition
meets the exciting future

Class Refinement as Semantics of Correct Object Substitutability

Ralph-Johan Back, Anna Mikhajlova, Joakim von Wright, Class Refinement as Semantics of Correct Object Substitutability. Formal Aspects of Computing 12, 18–40, 2000.

Abstract:

Subtype polymorphism, based on syntactic conformance of
objects' methods
and used for substituting subtype objects for supertype objects,
is a characteristic feature of the object-oriented programming style.
While certainly very useful, typechecking of syntactic conformance
of subtype objects to supertype objects is insuficient to guarantee
correctness of object substitutability. In addition, the behaviour
of subtype objects must be constrained to achieve correctness. In
class-based systems classes specify the behaviour of the objects
they instantiate. In this paper we define the class refinement relation
which captures the semantic constraints that must be imposed on classes
to guarantee correctness of substitutability in all clients of the
objects these classes instantiate. Clients of class instances are
modelled as programs making an iterative choice over invocation of
class methods, and we formally prove that when a class C0 refines
a class C, substituting instances of C0 for instances of C is refinement
for the clients.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jBaMiWra,
  title = {Class Refinement as Semantics of Correct Object Substitutability},
  author = {Back, Ralph-Johan and Mikhajlova, Anna and Wright, Joakim von},
  journal = {Formal Aspects of Computing},
  volume = {12},
  pages = {18–40},
  year = {2000},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Publication Forum rating of this publication: level 2

Edit publication