假设弱化性质

<p>在<a href="https://buttondown.com/hillelwayne/archive/some-tests-are-stronger-than-others/" target="_blank">有些测试比其他测试更强</a>一文中，我将 <code>STRONG => WEAK</code> 定义为“任何通过测试 STRONG 的系统也保证能通过 WEAK”。这使用了逻辑蕴含运算符，定义为 <code>P => Q = !P || (P && Q)</code>。</p> <p>蕴含可能是逻辑中被过度使用的运算符。除此之外，它还用于形式化规范，其中 <code>Spec => Prop</code> 表示“任何满足 <code>Spec</code> 的系统都具有属性 <code>Prop</code>”，而 <code>ASSUME => Spec</code> 表示“假设 <code>ASSUME</code> 必须成立，系统才能满足 <code>Spec</code>”。</p> <p>现在我们把它们混在一起做些数学推导。首先，“系统具有属性 <code>Prop</code>”等同于“系统通过了检查 <code>Prop</code> 的测试”，所以测试强度也是属性强度。现在让 <code>ASSUME => Prop</code> 表示“假设 <code>ASSUME</code> 为真时系统通过 <code>Prop</code>”。在经典逻辑中，如果 <code>P</code> 为真，那么显然 <code>!Q || P</code> 为真。进一步，这等价于（只需画出真值表！）<code>!Q || (P && Q)</code>。因此对于<em>任何</em>命题 <code>P</code> 和 <code>Q</code>，有 <code>P => (Q => P)</code>。</p> <p>换句话说，<code>Prop => (ASSUME => Prop)</code>。再换句话说，“系统通过 <code>Prop</code>” 是一个比“只要我们的假设成立，系统就通过 <code>Prop</code>”更强的性质。</p> <p>再再换句话说，任何添加的假设都会使性质变弱。</p> <p>这对我来说很直观。一个只经过 ASCII 字符串验证的 JSON 解析器具有的性质是“输入仅使用 ASCII && 是有效 JSON => 正确解析”。一个更好的、适用于所有 Unicode 的 JSON 解析器将具有“是有效 JSON => 正确解析”的性质，它假设更少，意味着保证在严格超集的情况下工作。</p> <p>这也符合“假设越多，出错可能性越大”的直觉。当 <code>Prop</code> 为假时我们遇到 bug。<code>Spec => Prop</code> 为真而 <code>Prop</code> 为假的唯一情况是 <code>Spec</code> 为假，例如我们的系统没有满足我们打算实现的规范。另一方面，当 <code>Spec</code> <em>和/或</em> <code>ASSUME</code> 为假时，<code>Spec => (ASSUME => Prop) && !Prop</code> 为真，这意味着即使正确实现的系统，如果运行时假设为假，也可能显示 bug。</p> <p>...回顾一下，最后两段有不少概念跳跃。你觉得有道理吗？对我来说一切都很自然，但这可能只是我熟悉这个话题的缘故。</p> <p>无论如何，关于假设还有几点说明：</p> <h2>我们为何使用假设</h2> <p>为什么不在我们的系统中满足 <code>ASSUME => Prop</code>，而是“直接”满足 <code>Prop</code>？至少三个原因。</p> <p><strong>第一</strong>，有时 <code>Prop</code> 根本无法满足，我们需要添加假设来使这一性质成立。我们在形式化方法中经常通过<a href="https://www.hillelwayne.com/post/fairness/" target="_blank">公平性</a>这样做。性质“<code>mergesort</code> 总是返回排序后的列表”是不可满足的，因为我们可以在它返回前把电脑踢飞。相反，我们必须验证一个较弱的性质，比如“<code>mergesort</code> 总是返回 => 它返回排序后的列表”或“<code>mergesort</code> 总是取得进展 => 它最终会返回排序后的列表”。</p> <p>另一个例子是 Rust。Rust <em>并不</em>保证性质“程序是内存安全的”。它保证较弱的性质“所有 <code>unsafe</code> 块都是内存安全的 => 程序是内存安全的”。让语言满足更强的性质会排除 Rust 的太多用例。注意，如果你不使用 <code>unsafe</code>，你也会获得内存安全，但这仍然满足假设，因为所有<em>零</em>个块都是安全的！</p> <p><strong>第二</strong>，有时强性质是可满足的，但额外成本不值当。比如让软件抗宇宙射线是可能的，但如果你的代码不是在太空运行，何必呢？只需说“没有宇宙位翻转 => 一切正常工作”。或者，如果你的插件适用于 Neovim <code>0.12</code> 但不适用于 0.11，你可能花功夫让它兼容旧版本，或者告诉大家需要升级才能使用你的插件。“Neovim 版本至少为 0.12 => 插件正常工作”。</p> <p><strong>第三</strong>，有时强性质在系统中是可满足的，但不容易<em>验证</em>。比如你的算法做了很多 API 调用，测试时不想触发速率限制。如果你<a href="https://en.wikipedia.org/wiki/Mock_object" target="_blank">模拟 API</a>，你测试的是较弱的性质“模拟对 API 足够准确 => 算法正确”。</p> <h2>假设是系统效应的第二层</h2> <p>我注意到最后两节中的几乎所有例子都是外部程序因素：</p> <ul> <li>JSON 解析器的假设是关于用户输入的</li> <li>公平性假设是关于操作系统/硬件/运行环境的</li> <li>Unsafe 假设是关于 Rust 编译器无法验证的事情</li> <li>宇宙射线假设取决于硬件的物理位置</li> <li>插件假设是关于 Neovim 团队的发布计划和社会兼容性契约</li> </ul> <p>边缘情况是用模拟替换第三方调用。这个假设是程序内部的，因为程序在测试中可以直接调用 API。我们仍然有这个假设是因为一个外部程序约束。也许这就是为什么模拟被视为敏捷开发中的反模式。</p> <p>一个后果是，检查假设是否成立与验证代码在假设下是否正确工作是不同的问题。例如，确保“所有 unsafe 块都是安全的”不能使用 Rust 编译器，你需要第二个工具如 <a href="https://github.com/rust-lang/miri" target="_blank">Miri</a>。我想知道在实践中检查假设是否通常比检查其他所有事情更困难。</p>