A general theory of semantic matches is developed that considers not only functions, but also modules consisting of functions. The authors assume that the behavior of a component is specified by a signature and by pre- and postconditions. Different questions of interest, such as retrieval, reuse, substitution, and subtyping, correspond to different definitions of matching; for example, exact pre/post match specifies interchangeable components, whereas plug-in match is asymmetrical. Weaker definitions ensure only that components have the same effect if the preconditions are checked separately. All the variants are derived from two definitions: one relates the preconditions of two components and their postconditions separately, whereas the other relates the specification predicates in their entirety. A clearly arranged table summarizes the results.

The core of the paper, section 3, is restricted to matching function specifications. On this basis, section 4 presents a parameterized definition of module matching. Section 5 reports on an implementation based on the Larch theorem prover, the syntax of which is briefly introduced in section 2. The last section is concerned with two applications. The first, a file cache manager, illustrates retrieval for reuse. The second considers determining when one object type is a subtype of another.

This clearly written research paper not only makes a theoretical contribution to specification matching, it also demonstrates the feasibility of this approach, although the examples are too small to convince readers that the technique can be put into practice in the near future. Nevertheless, I recommend the paper not only to researchers in this field but also to practitioners.