本文作者为 Amy Moormann Zaremski（施乐公司）和 Jeannette M. Wing（卡内基梅隆大学），发表于 ACM Transactions on Software Engineering and Methodology 1997 年第 6 卷第 4 期。文章围绕“软件构件的规格匹配（specification matching）”这一主题，系统提出了基于形式化规格说明来比较两个软件构件行为关系的理论框架、匹配定义、实现方法与应用场景。该研究属于软件工程、形式化方法与软件复用交叉领域，核心目标是在不运行代码的前提下，通过前置条件（precondition）和后置条件（postcondition）所构成的逻辑谓词来判断一个构件能否替换、复用或适配另一个构件。

论文首先明确了研究动机。在软件检索、复用、替换和子类型判断等任务中，仅依靠函数签名（signature）往往无法区分行为不同的构件。例如，C 语言数学库中大量函数具有相同的 double → double 签名，但语义完全不同。因此，作者主张使用以 Larch/ML 编写的先决条件与后置条件作为构件行为的形式规范，并通过定理证明来判断匹配关系。论文将构件建模为签名与规范的对偶 C = ⟨C_sig, C_spec⟩，并定义了通用的构件匹配谓词 Match(C, C') = Match_sig(C_sig, C'_sig) ∧ Match_spec(C_spec, C'_spec)，其中签名匹配作为低成本的过滤阶段，规格匹配则负责捕捉语义层面的关系。

在函数级规格匹配方面，论文提出了两大类与八种具体定义。第一类为“前置/后置匹配（pre/post match）”，其通用形式为 Match_pre/post(s,q) = (q_pre ⊇ s_pre) ∧ (ŝ ⊇ q_post)，其中前、后置条件之间的关系可以是等价（↔）或蕴含（→）。最严格的是“精确前置/后置匹配”（exact pre/post match），要求前置条件等价且后置条件等价，表示两个构件完全可互换。“插件匹配”（plug-in match）将两个等价关系都放松为蕴含，即查询构件 q 的前置条件蕴含库构件 s 的前置条件，且 s 的后置条件蕴含 q 的后置条件，从而保证 s 可以透明地替换 q。“插件后置匹配”（plug-in postmatch）进一步只要求后置条件的蕴含关系，忽略前置条件。“带保护插件匹配”（guarded plug-in match）在 plug-in match 的基础上，将库构件的前置条件作为附加假设引入后置条件的证明，以处理空容器等边界情况；“带保护后置匹配”（guarded postmatch）则只保留 s_pre ∧ s_post → q_post 的后置关系。第二类为“谓词匹配（predicate match）”，其通用形式为 Match_pred(s,q) = s_pred ⊇ q_pred，其中规范谓词 s_pred = s_pre → s_post。精确谓词匹配要求两个谓词等价；“泛化匹配”（generalized match）要求库规范谓词蕴含查询谓词，适用于查询较简单、库规范较详细的情形；“特化匹配”（specialized match）则反向要求查询谓词蕴含库谓词，可用于寻找实现目标构件的基础构件。论文将所有函数级匹配组织为一个格（lattice），明确各匹配之间的强弱关系。

在模块级匹配方面，论文将模块接口定义为用户自定义类型集合与函数抽象集合的二元组 ⟨T, F⟩，并定义了模块匹配 M-match((L, Q, match_fn))。其核心思想是：查询模块中的每个类型和每个函数都必须在库模块中找到一一对应，且类型匹配需满足重命名一致性，函数匹配则可由任意一个函数级规格匹配谓词实例化。该定义允许库模块比查询模块包含更多函数，从而支持查询者只关注部分功能。模块匹配的一个典型应用是面向对象中的行为子类型（behavioral subtyping）判断。

实现方面，论文基于 Larch Prover（LP）实现了自动生成匹配证明目标的工具链。该工具将 Larch/ML 规格翻译为 LP 输入，为每个函数生成 foo_pre 和 foo_post 两个算子，并将 trait 中的公理载入证明环境。论文中全部例子均在 LP 中完成验证。部分证明无需人工介入即可自动完成，例如 push 与查询 q2 的 plug-in match；部分证明则需要用户提供归纳策略或补充引理，例如 stack.top 与 q6 的 guarded plug-in match 需要通过对容器结构的归纳并实例化存在变量才可完成。

论文的结果主要通过六个示例查询和八个匹配定义展示。例如，查询 q1 描述了一个返回大小为 0 的有序容器的函数，在 exact pre/post match 下同时被 stack 与 queue 的 create 函数匹配，证明依赖于容器 length 与 empty 的等价推导。查询 q2 是返回大小增加 1 的弱添加函数，在 plug-in match 下由 push 和 enq 匹配，因为库前置条件为 true 且后置条件可由 size(insert(e,q)) = size(q)+1 直接得出。查询 q4 要求删除后容器大小减 1 但不指定删除哪个元素，在 guarded plug-in match 下由 pop 和 rest 匹配，因为需要排除空容器情形。查询 q6 要求返回最后插入的元素，在 generalized match 和 guarded plug-in match 下匹配 stack.top，但不匹配 queue.deq。这些例子共同表明：越强的匹配定义提供越严格的行为保证，也越难满足；而带保护的匹配能在不牺牲健全性的前提下适应边界条件。

在应用层面，论文讨论了复用检索与行为子类型两个场景。检索问题被形式化为 Retrieve(q, match_spec, L) = {c ∈ L | match_spec(c, q)}。文件缓存管理器示例展示了 guarded plug-in match 如何允许用户用较弱查询同时检索到 FIFO 策略的 replacefirst 和优先级策略的 replacemax 两个实现。行为子类型以 bag 与 stack 对象规范为例，说明 stackobj 是 bagobj 的行为子类型，其关键是方法级采用 guarded plug-in match 来排除空容器情况，并通过模块匹配建立方法之间的映射。

论文的主要贡献包括：第一，系统提出统一的规格匹配理论框架，涵盖函数与模块两个层次、精确与松弛多种匹配定义；第二，给出了具有模块化结构的实现工具，使得同一框架可以替换不同函数匹配谓词或扩展签名匹配；第三，将规格匹配从软件检索扩展到行为子类型等领域。研究价值在于为软件复用中的语义比较提供了严格的逻辑基础，也为程序替换和类型系统设计提供了可自动化的验证路径。其方法的新颖之处在于把函数级匹配参数化地嵌入模块匹配，并通过定理证明技术把定义直接转化为可执行的验证流程，而不是仅停留在理论层面。这一工作为后续体系结构失配、协议匹配以及更丰富的接口规范扩展奠定了方向。