假设会削弱属性保证Assumptions weaken properties

在某些测试中，我定义 STRONG => WEAK 表示“任何通过 STRONG 测试的系统也一定能通过 WEAK 测试”。这里使用了逻辑蕴含运算符，其定义为 P => Q = !P || (P && Q)。

蕴含可能是逻辑中最被过度使用的运算符之一。它在形式化规范中也频繁出现，例如 Spec => Prop 表示“满足规范 Spec 的系统具有属性 Prop”，而 ASSUME => Spec 则表示“系统要满足规范 Spec，必须假设 ASSUME 成立”。

现在我们把这些概念结合起来做些数学推导。首先，“系统具有属性 Prop”等同于“系统通过了检验 Prop 的测试”，因此测试强度也反映了属性强度。现在令 ASSUME => Prop 表示“在假设 ASSUME 为真的前提下，系统通过 Prop”。在经典逻辑中，若 P 为真，则显然 !Q || P 也为真；进一步地，这与 !Q || (P && Q) 等价（只需画真值表即可验证）。因此对任意命题 P 和 Q，都有 P => (Q => P)。

换句话说，Prop => (ASSUME => Prop)。换言之，“系统通过 Prop”这一性质比“在假设成立时系统通过 Prop”更强。

再换句话说，添加任何假设都会使属性变弱。

这对我来说很直观。一个仅针对 ASCII 字符串验证过的 JSON 解析器具有如下属性：“输入仅使用 ASCII 且是有效 JSON ⇒ 被正确解析”。而一个支持所有 Unicode 的更好解析器则具有“是有效 JSON ⇒ 被正确解析”的属性，它依赖的假设更少，意味着它能保证在更广泛的用例中正常工作。

这也符合“假设越多越容易出错”的直觉。当 Prop 为假时就会出现 bug。Spec => Prop 为真而 Prop 为假的唯一情况是 Spec 为假，即我们的系统并未实现我们原本打算实现的规范。另一方面，只要 Spec 或 ASSUME 中至少有一个为假，Spec => (ASSUME => Prop) && !Prop 就为真，这意味着即使系统实现正确，一旦运行时假设不成立，仍可能出现 bug。

...回头再看最后两段，中间有不少概念跳跃。这些对你来说都合理吗？虽然我觉得很自然，但这可能只是因为我对此话题比较熟悉罢了。

无论如何，关于假设还有几点补充说明：

为什么我们需要假设？

为什么不干脆直接构建满足 ASSUME => Prop 的系统，而非得去“仅仅”构建满足 Prop 的系统呢？至少有三个原因。

首先，有时 Prop 本身根本无法满足，我们必须引入假设才能使该属性成立。这在形式化方法中非常常见，尤其是在处理公平性时。例如“归并排序总能返回有序列表”这个属性是不可满足的——因为可能在它返回前就把电脑踢飞了。所以我们转而验证较弱的属性，比如“归并排序返回结果 ⇒ 结果是排好序的”，或者“归并排序持续进展 ⇒ 最终会返回一个有序列表”。

另一个例子是 Rust 语言。Rust 并不保证“程序内存安全”这一强属性，而是保证较弱的属性：“所有 unsafe 块都是内存安全的 ⇒ 整个程序是内存安全的”。如果让语言本身满足更强的属性，就会排除太多 Rust 的使用场景。值得注意的是，即便不使用 unsafe，也能获得内存安全性，而这仍然满足假设条件——毕竟零个 unsafe 块本身就是安全的！

其次，有时强属性是可满足的，但实现成本过高。比如可以让软件具备抵御宇宙射线的能力，但如果你的代码并不在太空中运行，那何必费心呢？直接声明“无宇宙射线比特翻转 ⇒ 程序正常运行”即可。或者，如果你的插件支持 Neovim 0.12 但不兼容 0.11，你可以选择投入精力使其兼容旧版本，也可以干脆要求用户升级到新版本才能使用插件——即声明“Neovim 版本至少为 0.12 ⇒ 插件正常工作”。

第三，有时强属性在系统中是可满足的，却难以验证。例如，若你的算法频繁调用 API，而测试时又不想触发速率限制，那么你可以通过模拟（mock）API 来测试较弱的属性：“模拟准确反映真实 API 行为 ⇒ 算法正确”。

假设是系统影响的第二层

我注意到前两部分几乎所有例子都属于外程序因素（exoprogram factors）：

边界情况是用模拟替换第三方调用。此时假设属于内程序（intraprogram），因为程序本可以直接调用 API 进行测试。但由于存在外程序约束，我们仍需做出该假设。或许这就是为什么在敏捷开发中，模拟常被视为反模式的原因之一。

一个结果是：判断假设是否成立是一个不同于“在给定假设下验证代码是否正确”的问题。例如，要确保“所有 unsafe 块都是安全的”不能仅靠 Rust 编译器，还需要像 Miri 这样的额外工具。我在想，在实践中，检查假设是否成立是否通常比检查其他所有内容都更难。