To appear ACM Transactions on Software Engineering and Methodology (TOSEM), 1997.
The full text of this paper is here (in PostScript).
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 post-conditions 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.