最近我做了大量 Alloy 相关的工作，这让我开始思考一个常见的规约陷阱。正文中的所有内容都适用于各种形式化规约，折叠框里的内容则是写给有经验的 Alloy 用户看的。

我们来看一个依赖树的简单模型。假设程序有一组顶层依赖，每个依赖又有自己的依赖，以此类推。在 Alloy 中可以这样建模：

sig Package {
  , depends_on: set Package
}

run {some depends_on}

abstract sig Package {
  , depends_on: set Package
}

lone sig A, B extends Package {}

run {some depends_on}

如果翻看 Alloy 生成的一些实例，会发现一件奇怪的事：一个包竟然会依赖它自己！

在做规约时，这种不合常理的情况经常出现，因为我们心里对系统应该是什么样子有一个预期，却没有把它明确地写进模型。当出现这种情况时，就需要添加额外的约束来避免它。为此，Alloy 提供了一个专门的关键字“fact”：¹

fact no_self_deps {
    all p: Package {
       p not in p.depends_on 
    }
}

fact {
    no depends_on & iden
}

Alloy 不会生成任何违反 fact 的实例，也不会在这些实例中去寻找不变式违例。它把 fact 当作“现实中的事实”，认为根本无需探索。

fact 的陷阱

“禁止自依赖”是一个典型的 fact 例子，同时也是一个糟糕的 fact 例子。新手经常会犯这样的错误：用 fact 来对系统建模，这很快就会引发问题。

先暂时抛开规约，想想真实的系统。包管理器的依赖是从哪来的？通常是一个像 package.json 或 Cargo.toml 这样的纯文本文件。如果有人手动在文件里写了一个自依赖会怎样？按理说，你会希望包管理器能检测到这种自依赖，并将其作为错误拒绝。你怎么知道错误处理是有效的呢？就是让检查器去验证：它能接受合法的清单，并拒绝带有自环的清单。

可惜它现在无法测试这种拒绝逻辑，因为我们已经告诉它不要生成任何自依赖。我们的 fact 让自依赖变得无法表示了。

在编程语言中，“让非法状态不可表示”（MISU）通常是一件好事（1 2 3 4）。但规约所涵盖的不仅是你正在编写的软件，还包括软件运行的环境，也就是机器与世界。如果无法表示非法状态，也就无法表示世界产生了需要你的软件去处理的非法状态。

相比 fact，你更应该使用谓词。然后你就可以测试谓词为真时的情况，或检查它是获得其他性质的必要条件。让约束显式化，而不是隐式化。

// instead of

fact no_self_deps {/*body*/}

run {some_case}
check {some_property}

// do

pred no_cycles {/*body*/}

run {
  no_cycles and some_case
}

check {no_cycles implies some_property}

谓词还有一个额外的好处，就是“局部作用域”：如果你有三条 fact，却想只用其中两条来检查模型，就不得不把第三条注释掉。

什么时候该用 fact

那么，我们到底该在什么时候使用 fact？在什么情况下，全局强制约束才是合理的，即使这样做可能会削弱我们的模型？

第一，fact 适合用来缩小问题的范围。如果我们只对包安装器做规约，而清单的校验由另一部分负责，那么“禁止自依赖”就是一条完全合理的 fact。把它写成 fact，可以明确地告诉读者：我们不负责校验清单。这意味着当这个假设不成立时，我们不作任何保证。

第二，fact 可以用来排除那些根本无需关注的情况。比如我在对链表建模：

sig Node {
  next: lone Node //lone: 0 or 1
}

这个模型会生成普通链表和带环的链表，这两种情况对我来说都是有意义的，我不想把任何一种约束掉。但它也会生成包含两个互不相连链表的模型。如果我只关心单条链表，就可以用一条 fact 来排除多余的链表：

fact one_list {
    some root: Node | root.*next = Node
}

open util/graph[Node]

fact {
    weaklyConnected[next]
}

类似地，你也可以用 fact 来消除无关的细节。比如在对用户和组建模时，我不想要任何空组，就会添加一条像 Users.groups = Group 这样的 fact。

第三，你可以用约束来优化运行缓慢的模型，通常是通过对称性破缺来实现。

最后，你可以用 fact 来定义那些 Alloy 无法直接表达的必要关系。在我参与的一个项目中，图里有红色和蓝色两种节点。红色节点至少有一条边连向其他节点，蓝色节点至多有一条边。我们本来是这样写的：

abstract sig Node {
}

sig Red extends Node {
  edge: some Node
}

sig Blue extends Node {
  edge: lone Node
}

但这样一来，我们就无法编写通用的、使用了 edge 的节点谓词，因为 Alloy 会将其视为类型错误。于是我们改用 fact 来写：

abstract sig Node {
  edge: set Node
}

sig Blue, Red extends Node {}

fact {
  all r: Red  | some r.edge
  all r: Blue | lone r.edge
}

module main

// spec

check {spec => always (prop1)}
check {spec => always (prop2)}

// etc

open main

fact {spec}

check {always (prop1)}
check {always (prop2)}
// etc

结论

约束是危险的，因为你需要错误状态，才能去检查程序是否避开了错误状态。

如果你想进一步学习 Alloy，这里有一本不错的书，而且我也维护了一份参考文档。我还在筹备一个新的 Alloy 研讨会，上个月刚完成了内测，计划今年夏天晚些时候进行公测。欢迎订阅我的邮件简报以获取最新动态！

感谢 Jay Parlar 和 Lorin Hochstein 提供的反馈。如果你喜欢这篇文章，欢迎订阅我的邮件简报！我每周都会在上面发布新的文章。

我为企业提供形式化方法培训，帮助软件开发变得更快、更便宜、更安全。点击这里了解更多。

1. 在其他规约语言中，这通常要么是运行时约束（如 TLA+ 中的做法），要么是对系统规约本身的直接修改。[返回]