Computer Things

2025年4月24日

需求变化到不变

Requirements、阶段变化和 Formal Methods

最近我收到了一个关于 Formal Methods 的问题：当系统 Requirements 不断变化时，对系统进行数学建模有什么帮助？ 花费大量时间来证明一个设计是可行的，然后交付产品，却发现它根本不是客户所需要的，这没有任何意义。 正如俗话所说，最难的部分是“构建正确的东西”，而不是“正确地构建东西”。

一个可能的回答是：“为什么要编写测试”？ 如果你可能会在 Requirements 发生变化时将它们全部丢弃，那么你不应该编写测试，_尤其是_提前编写大量的单元测试。

这是一个糟糕的回答，因为我们都知道编写测试和使用 Formal Methods 的区别：测试 容易 而 FM 难。 测试需要较低的成本来实现中等的正确性，而 FM 需要较高（ish）的成本来实现高度的正确性。 当 Requirements 不断变化时，“较高（ish）的成本”是无法承受的，而“高度的正确性”也是不值得的，因为一个能够解决客户问题的还算可以的解决方案，比一个不能解决问题的可靠解决方案要好得多。

但最终你会得到一些能够解决问题的方案，然后呢？

我们大多数人都不为 Google 工作，我们不能随意砍掉功能和产品。 如果客户对你的解决方案感到满意，那么你就需要支持它。 当你的客户遇到新的边缘情况，或者将所有计算机迁移到下一个 OS 版本，或者扩展到互联网很差的市场时，它应该能够正常工作。 当 10 倍的客户使用 10 倍的功能时，它应该能够正常工作。 当你添加发生冲突的新功能时，它应该能够正常工作。

而且同样重要的是，它应该永远不要停止解决他们的问题。 典型的例子：你的功能涉及同步处理请求的任务。 在大规模情况下，这不起作用，因此为了提高延迟，你将其更改为异步处理。 现在它最终是一致的，但你的客户依赖于它始终保持一致。 现在它不再满足他们的需求，并且已经停止解决他们的问题。

每个成功的 Requirement 都会产生一个新的 Requirement：“保持这个功能正常工作”。 这个 Requirement 是永久性的，或者足够接近永久性，可以用来决定我们的长期战略。 需要积极投入才能保持一个功能与周围世界的变化保持一致。

（这是否只是一个用自命不凡的方式说“软件维护很难”的说法？ 也许吧！）

阶段变化

在物理学中，有一个相变的概念。 要将一克液态水的温度升高 1°C，你必须添加 4.184 焦耳的能量。 这会持续到你将其升高到 100°C，然后它会停止。 在你向该克水中添加了两 千 焦耳的能量后，它会突然变成蒸汽。 系统的能量连续变化，但形式或阶段会离散变化。

Phase_diagram_of_water_simplified.svg.png (from above link)

软件不是物理学，但这个想法可以作为一个隐喻。 某种架构可以处理一定程度的负载，超过这个负载你需要一个新的架构。 或者一堆类似的功能被独立地硬编码，直到系统变得过于混乱而无法理解，你会将内部结构重塑为统一的、可扩展的东西。 等等。 它不必是完全离散的阶段变化，但系统中肯定有“之前”和“之后”。

阶段变化往往会导致系统更加复杂，这意味着阶段变化可能会将新的 Bug 引入到现有行为中。 以同步与异步的情况为例。 一个非常简单的同步更新玩具模型是 Set(key, val)，它将 data[key] 更新为 val。 一个异步更新的模型是 AsyncSet(key, val, priority)，它将一个 (key, val, priority, server_time()) 元组添加到 tasks 集合中，然后另一个进程异步地拉取一个元组（按最高优先级排序，然后按最早时间排序）并调用 Set(key, val)。 以下是客户可能需要保留的一些属性作为 Requirement：

如果新系统不满足现有的客户 Requirement，那么在发布新系统_之前_修复 Bug 是明智的。 客户不会注意到或关心你的系统是否经历了阶段变化。 他们只会看到有一天你的产品解决了他们的问题，而第二天它突然就不能解决问题了。

这是 Formal Methods 最常见的应用之一。 这两个系统以及每个属性都可以在规范语言中正式指定。 然后我们可以自动检查新系统是否满足现有属性，并从那里执行自动生成测试套件之类的操作。 这确实需要大量的工作，所以如果你的 Requirements 不断变化，那么 FM 可能不值得投资。 但最终，Requirements 会_停止_变化，然后你就会永远被它们困住。 这就是模型发挥作用的地方。

如果网络上阅读此内容，可以在这里订阅。 每周更新一次。 我的主要网站是这里。

我的新书《程序员逻辑》（Logic for Programmers）现在可以提前阅读了！ 在这里获取。