Specification Matching of Software Components
ACM Transactions on Software Engineering and Methodology, 6 (4):
333--369 (October 1997)Abstract
Specification matching is a way to compare two software components,
based on descriptions of the component's behaviors. 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. 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, and substitutability of software components. Since our
formal specifications are pre- and postconditions written as
predicates in first-order logic, we rely on theorem proving to
determine match and mismatch. We give examples from our implementation
of specification matching using the Larch Prover.
