Specification Matching of Software Components
Authors: Amy Moormann Zaremski and Jeannette M. Wing
CMU-CS-95-127. Also submitted to SIGSOFT '95 Foundations of
Software Engineering Symposium, 1995.
The full text of this paper is here (in
Specification matching is a way to compare two software components.
In the context of software reuse and library retrieval, it can help
determine whether one component can be substituted for another or how
one can be modified to fit the requirements of the other. In the
context of object-oriented programming, it can help determine when one
type is a behavioral subtype of another. In the context of system
interoperability, it can help determine whether the interfaces of two
We use formal specifications to describe the behavior of software
components, and hence, to determine whether two components match. We
give precise definitions of not just exact match, but more relevantly,
various flavors of relaxed match. These definitions capture the
notions of generalization, specialization, substitutability,
subtyping, and interoperability of software components.
We write our formal specifications of components in terms of pre- and
post-condition predicates. Thus, we rely on theorem proving to
determine match and mismatch. We give examples from our
implementation of specification matching using the Larch Prover.