本文记录了一次关于”如何对软件质量问题进行分类”的对话式探索。起点是一个朴素的四分法,终点是一个被拆解、重构后的二维模型。我把它写下来,不是因为得到了终极答案,而是因为这个修正过程本身比最终的结论更有价值 —— 它暴露了软件工程社区里几个被广泛使用但从未被严格审视的概念(规格、契约、性质)之间真实的结构关系。
最初我提出,任何质量问题都应该能归入以下四类之一:
这个四分法的吸引力在于:它把”质量”从模糊的工程直觉,翻译成可被多维度审问的命题。每发现一个 bug,你都能沿着这条轴回溯,找到缺口。
但这个框架的完备性,取决于”契约”是窄义还是宽义。
在 Meyer 的 Design by Contract(契约式设计)语境下,”契约”是一个相对窄的概念:专指方法级别的前置条件、后置条件、类不变式。它和”方法签名”(类型层面的契约)相对,强调的是语义层面的约束。
但日常工程里,我们更习惯把”契约”做宽义使用:涵盖功能契约、SLA、不变式、架构约束等所有”系统应满足的性质”。
这个语义宽窄的冲突,是后续所有混淆的根源。
我一度试图用”形式化程度”来切分规格(低形式化)和契约(高形式化)。但这个切分立刻被反例击穿:
/** transfer 要求 from.balance >= amt */ —— 纯自然语言,但它是契约。媒介(散文 vs 形式化)不决定归属。契约可以在任何载体上存在;规格也可以高度形式化。
我反复试错后发现,区分契约和规格的判据不是”形式化程度”,而是义务的结构:
| 判据 | 契约 | 规格(非契约部分) |
|---|---|---|
| 义务方 | 双边:调用方背前置,被调用方背后置 | 单边:描述系统性质,无对手方 |
| 接口锚定 | 钉在具名接口上(函数、API、消息类型) | 自由漂浮,不依赖任何代码位置 |
| 推理方式 | 局部 + 组合推理(只需契约即可推理组合) | 全局推理(验证时需纳入整个系统) |
一句话:契约是绑定双边义务、锚定接口的规格。
“双边义务”与”锚定接口”是核心,且二者往往共生:双边义务必然要求一个具名接口(谁和谁签?)。而表格第三行的”推理方式”描述的其实是契约带来的能力差异(契约允许局部推理,规格需要全局推理)——这种能局部推理的能力,通常被称为可组合性,它更像一个衍生的能力,而非又一条独立判据。它通常由”双边义务 + 锚定接口”的结构所 enabling,但不是非黑即白的开关:无状态函数契约的组合性强,有状态对象契约的组合性弱,统计性 SLA 的组合性近乎为零。换句话说,”可组合性”是一条光谱,而非二元判据。这点在下面会反复回来咬我们。
如果契约的核心是”绑定双边义务 + 锚定接口”(并衍生出组合推理的能力),而规格是更宽泛的”系统应满足什么的陈述”,那么:
契约 ⊂ 规格。契约就是规格的一种特化形式,就像正方形是矩形的特化形式。
这不是模糊,这是正确的分类学结论。我们之前感觉”规格和契约边界模糊”,是因为我们试图在两者之间找一条阶段边界(它们分别属于流程的哪一步),但它们根本不在阶段轴上竞争位置 —— 它们在同一阶段,只是贴了不同的标签。
如果契约只是规格的一个子集,那”规格中除契约之外的部分”是什么?
诚实答案是:没有统一的专名。因为它是”异质的剩余类”,包含了四种性质迥异的东西:
| 子类 | 例子 | 子社区里的专名 |
|---|---|---|
| 系统级不变式 | “余额永不为负”、”无死锁” | 不变式 (Invariant) |
| 质量属性 | “p99 < 100ms”、”MTBF > 10000h” | 质量属性 (Quality Attribute) |
| 架构约束 | “无循环依赖”、”读写分离” | 架构约束 (Architectural Constraint) |
| 领域规则 | “订单金额 = 单价 × 数量 − 优惠” | 领域规则 (Domain Rule) |
注意这些子类并非互斥:同一陈述常可同时归入多类(“余额永不为负”既是领域规则也是不变式)。列出它们只为展示异质性,不是干净分类。
实践中的处理方式是:不要试图统一命名,根据具体子类用各自的专名。
最初的直觉是把质量保证描述为一条线性的链条:
意图 → 规格 → 契约 → 性质 → 验证
契约和规格在同一个阶段,它们不应该并列出现在链条上——这条链条实际上把多个本应正交的轴强行压成了一条线。拆开后能看清楚四个维度:
其中(2)(4)并非完全独立——双边义务几乎必然要求一个具名接口,所以它们是半耦合的;(1)与(3)在流程两端也有强相关(意图期偏自然语言,验证期则必然形式化),只在中间的规格/性质阶段才真正两可。把它们硬压成一条线,就是错误的开端。
把维度分开后,模型立即清晰:
水平轴(唯一的链条):
意图 → 规格 → 性质 → 验证
结构标签(可贴在流程任何阶段):
契约不是链条上的独立阶段,而是规格阶段里贴了 绑定接口 + 双边义务 标签的特例(“可组合性”是这对结构衍生的能力,不单独计入标签)。
“规格和契约的边界在哪”这个问题之所以无解,是因为它问错了维度 —— 它们本来就在同一个阶段,只是在标签轴上取了不同的值。
“性质”(property)在形式化方法里本指全称命题:forall x ∈ Domain. P(x)。它不可执行(无法遍历无限域),只能被证明或被反例反驳。
但 QuickCheck 借走这个词命名了它的技术(“property-based testing” / 属性测试)。为什么会发生这种窄化?因为属性测试的工具可得性远高于形式化方法(装一个 QuickCheck 就能写 property,写 Coq 定理的门槛则高一个数量级),于是大众接触 property 这个词几乎全是经属性测试这条路径。久而久之,”property” 默认让人想到”一段可执行的、给框架去反驳的函数”,而不是”一个全称命题”。
严格说这不是篡改——PBT 里 property 的用法(forall input. P(input))与形式化方法的本义其实是连续的,只是被锚定到了采样验证这一种手段上。但词义窄化的代价是真实的:它让人误以为”性质”和”属性测试”是同义反复,从而看不见这中间存在一个可被独立讨论的投影层。
剥离这种词义窄化后,”性质”层的真实职责是:把契约(或规格)投影为可证伪命题。
forall input. P(input) 形式的全称命题属性测试只是性质的众多验证手段之一,不是性质本身。你可以写下一个性质却永远不测它(比如哥德巴赫猜想) —— 性质在概念上先于测试存在。
如果只用单元测试和运行时断言,性质层似乎是隐式的、甚至不存在 —— 你直接从契约挑具体输入写 assert f(3) == 9,中间没有”性质”工件。
但严格说,投影这一步在任何验证中都要发生,只是被折叠了:
prop_X)。x=3,隐式声明了”对 3 而言应该…”)。所以”性质”层不是”引入的复杂性”,而是”被折叠隐藏的步骤”。它在概念上总是存在,只是显式与否。把它显式化有认知价值(强迫你思考”契约对什么输入应该成立”),这是方法论收益;但在只用单元测试的体系里,把它折叠进测试用例,并无损失。
唯一例外:如果你的验证体系包含形式化证明,性质(全称命题本身)是证明器的入口工件,不能折叠——必须作为独立陈述存在(在 Coq 里就是 Theorem 语句),证明器对它做逻辑推导,根本不经过判定器。这是形式化方法社区坚持”性质”必须独立命名的根本原因。
意图 → 规格 → 性质 → 验证
应然 陈述 可证伪 可执行
这是唯一的链条,有方向,有依赖。每个工件是上一个的精细化。”性质”在概念上总是存在(详见第四节)。
三个标签(半独立)可贴在流程任何阶段:粒度(全局/绑定接口)、形式(自然语言/形式化)、义务(单边/双边)。
契约 = 规格 + [绑定接口] + [双边义务]。”支持组合推理”不是独立第四判据,而是这对结构的衍生能力(强弱成光谱)。
这个定义比日常宽义用法(把 SLA、不变式都算契约)更窄。以 SLA”该接口 p99 < 100ms”为例:它是单方向的服务承诺,缺乏”调用方做什么 ↔ 被调用方保证什么”的双边条件结构,因此按本文定义它不是契约、而是统计性的非契约规格。注意,这里排除 SLA 靠的是”双边义务”缺失,而非”可组合性”缺失——因为后者是光谱,用它作二元开关会误伤大量有状态的、组合性受限的公认契约(如带可变状态的栈)。这正是我们把”可组合”留作衍生能力、不升格为必要判据的原因。
非契约规格(全局不变式、质量属性、架构约束、领域规则)各自有专名,不需要也不应该强行统一命名。
原四分法被重构为对”流程轴上某点的标签”的审问:
给定一个 bug,问:
这个二维矩阵比原来的四分更精确,因为它区分了”哪个阶段出了问题”和”这个阶段的工件结构对不对”。
修正后的模型里,规格阶段包含契约和非契约两类。它们都可以下降到性质和验证,但下降的难易程度差异巨大:
这不是”非契约规格下不去”,而是”它们各自走向了不同的下游机器,而那些机器要么昂贵、要么统计性、要么工具链割裂”。
实践中,工程界用脚投票,集中投入在性价比最高的契约下降上。但这会漏掉一类致命的 bug:契约被完美执行,但系统仍然出错 —— 比如每个模块都正确履行了自己的契约,组合起来却违反了某个没被下降的系统不变式。
契约是下降的主战场,覆盖了绝大多数日常 bug,但识别系统的关键不变式并对它们单独下降(即使贵),是守住剩下那部分致命 bug 的唯一办法。
这次探索最有价值的不是得到了一个”更正确的分类法”,而是观察到一个朴素的工程直觉,是如何在反复的拷问下,逐步暴露其隐含维度,并最终被重构为更精确的模型。最初的四分法并不”错”——对功能正确性的日常诊断,它仍然是一个锋利的快速启发式。但拷问过程本身,让我们看清了”规格/契约/性质/验证”这几个被广泛使用却从未被严格审视的概念,各自的真实结构位置。
软件工程里,大多数方法论之争,本质上都是概念定义权之争。把概念的真实结构摊开来,比争论哪个方法论更”对”更有建设性。