非法状态 vs 不良状态Illegal vs Unwanted States

非法状态是我们绝不愿让系统进入的状态。不良状态是我们不想停留的状态。许多我们希望将其定为非法的状态，实际上只是不良状态而已。

考虑一个日历软件，它将日历事件存储为 {user: {events: [event]}} 的形式，其中每个事件都有开始和结束时间。这允许一个人同时参加两个事件。我们可能会认为这是非法的，并改用 {user: {time: optional event}} 的数据类型来避免这种情况。然而，日程冲突并不违法，只是不良！一个人完全可能报名参加两个时间重叠的事件。也许他们本应二选一，也许他们会稍后决定去哪个，或者其中一个事件实际上并不代表面对面的会议。

在这种情况下，停留在不良状态是可以接受的，尽管不是理想状态。其他不良状态如果不迅速退出，会导致无效状态。如果预订乘客人数超过座位数，航班就处于不良状态。这必须在乘客实际登机前解决，因为“飞机上实际乘客数超过座位数”是非法状态。

在某些情况下，不良状态不会导致非法状态，但长期停留在不良状态仍然是个问题。我们或许能保证网络分区不会导致数据不一致。即使网络分区这种不良状态不会引发数据损坏这种非法状态，但如果我们永远不修复分区，仍然会面临大问题。

为什么系统必须表示不良状态

一般来说，当我们无法完全控制系统行为时，不良状态就会出现。我们无法保证网络绝对可靠、服务器始终在线、用户输入正确数据。如果系统接收来自外部世界的输入，世界就可能将我们推入不良状态。我们需要能够检测这些状态，以便加以解决。

即使我们能完全控制系统，有时仍希望暂时进入不良状态。航空公司本可以杜绝超售机票。但航空公司之所以愿意超售，是因为他们预计会有部分乘客爽约。我们需要允许他们处于这种不良状态，然后建立机制防止其演变为非法状态。

有时我们需要不良状态来实现某些工作流程。95%的用户可能永远都不想接受冲突事件，禁止这种不良状态会让他们的生活更轻松。但没有这种不良状态，就无法故意重复预订。有些人确实需要这个功能！在这种情况下，我们要明确告知用户他们正处于不良状态，然后让他们自己决定是否以及如何离开该状态。

（航空公司和用户其实想要不良状态！是我们工程师觉得它"不良"，因为它可能带来后续问题。）

不良状态的正式模型

非法状态对应被违反的不变量。传统写法是 []!Illegal：Illegal 应该始终为假。只要有任何状态满足 Illegal，我们的系统就有 bug。

不受欢迎的状态更难处理，因为它们可能同时涉及安全性和活性属性。例如，在建模航空系统时，我们不一定需要检查超售相关的属性，而只需确保不会出现航班超载的情况。1 在验证过程中可能会发现，超售是导致航班超载的主要原因，或者如果不解决超售问题，最终必然会发生航班超载。此外，如果“永不超售”能保证“永不航班超载”，我们会认为“无超售”这一属性比“无航班超载”更强。

“我们永远不会处于网络分区状态”的形式化表达为 []<>!Partition：系统可以进入分区状态并长时间保持分区，但最终必须恢复连接。P 规范语言将这些状态称为热状态（hot states）。

（附注：如果一切顺利，下周应该会发布面向程序员的新版 Logic for Programmers！）