规格与实现的鸿沟，才是 Bug 的藏身之处
大多数软件 Bug 藏在规格描述与代码实际行为之间的缝隙里，看看形式化规格如何缩小这道鸿沟。
James Whitfield
编程语言理论圈子里时不时会冒出一个说法：‘足够详细的规格说明，与代码没有区别。’这个观点很有挑衅意味，暗示着‘描述程序应该做什么’和‘让程序真正去做’之间的界线，比我们想象的要薄得多。如果你的规格精确到足以消除所有歧义，那你其实已经把程序写出来了。
这不只是哲学空谈。它对我们构建软件的方式、规格在其中扮演的角色，以及为什么大多数 Bug 并非编码错误，而是规格缺口，都有实际影响。搞清楚规格在哪里结束、实现从哪里开始，会改变你对测试、类型和正确性的思考方式。
大多数 Bug 到底从哪来
问一个开发者 Bug 从哪来，他多半会说‘代码’。但大量软件缺陷的研究表明，情况并非如此：大多数 Bug 产生于意图与实现之间的缝隙。代码正确地执行了开发者交代的事情，问题在于规格（无论是形式化的还是非正式的）本身含糊、不完整或被误解了，开发者才让它去做了错误的事。
一个经典例子：规格写着‘系统应当处理并发请求’。‘处理’到底是什么意思？按顺序处理？同时处理？请求太多时排队？‘太多’是多少？队列满了之后到达的请求怎么办？这些问题不是实现细节，而是规格缺口。每一个没有回答的问题都是潜在的 Bug，因为开发者会通过实现隐式地作答，而他的答案未必符合用户或其他开发者的预期。
规格精确度的光谱
规格从非正式到形式化，构成一条连续的光谱。
- 自然语言。‘登录系统应当既安全又好用。’这几乎不算规格，更像是一种愿望。每个词都有歧义。什么算‘安全’？什么算‘好用’？这些都是伪装成需求的主观判断。
- 结构化自然语言。‘用户在 10 分钟内连续输错三次密码，则将账户锁定 30 分钟。’比前者精确，但仍然有歧义。‘输错密码’是否包括空提交？三次尝试必须是连续的吗？10 分钟的窗口是滚动的还是固定的？
- 类型签名。
authenticate(username: string, password: string) -> Result<User, AuthError>。它精确地规定了函数的接口，但对行为只字未提。你知道输入和输出的形状，却不知道二者之间的关系。 - 基于属性的规格。‘对于数据库中所有合法的用户名-密码对，
authenticate都返回Ok(user)，且user.username == username。’这里用逻辑量词对行为做了更精确的约束。 - 形式化规格。对系统行为的完整数学建模，涵盖每一个状态、每一次迁移和每一个不变式。到了这一层，规格和实现几乎就是同一个东西。
越接近形式化规格，留给歧义的空间就越小，留给 Bug 的空间也越小。但每往前一步，所需的投入和专业技能也越多。实际的问题是：对于某个具体项目，你应该沿着这条光谱走到多远？
类型作为轻量级规格
类型系统是日常编程中应用最广泛的规格形式。它们不描述行为，但会约束行为。一个返回 Option<User> 而不是 User 的函数，等于声明它可能找不到用户，而编译器会强制每个调用方都处理这种可能性。
// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User // What if ID is invalid?
// // What if user not found?
// // Does it panic? Return null?
// // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.Rust、Haskell 和 TypeScript 等语言表明，表达力强的类型系统无需形式化方法的训练，也能缩小规格缺口。代数数据类型、泛型约束和穷尽的模式匹配共同在类型层面规定了大量程序行为，而且编译器会自动验证。
关键在于：每一条类型标注都是一份会被自动检查的规格。你能在类型系统中编码的每一点行为，都意味着一类你永远不会遇到的 Bug。
基于属性的测试：规定行为
单元测试是基于示例的规格：‘给定这个特定输入，期望这个特定输出。’它们很有用，但本质上是不完整的，你只能测试自己想到的情况。基于属性的测试则反其道而行之：你规定对所有输入都应成立的属性，再由测试框架生成随机输入去寻找违反的情况。
from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.这个测试中的三条属性不只是在测试排序，它们定义了排序。任何满足这三条属性的函数，按定义就是一个正确的排序。这是‘规格即代码’理念最实用的体现：编写定义正确行为的属性，然后让测试框架去验证你的实现是否满足它们。
TLA+ 与模型检验
对于 Bug 代价高昂的系统，比如分布式系统、金融平台和关键基础设施，TLA+ 这类形式化规格工具能提供更强的保证。TLA+（Temporal Logic of Actions，动作时序逻辑）允许你把系统行为描述为状态机，然后进行模型检验：穷举探索每一种可能的执行路径，验证不变式是否成立。
亚马逊已用 TLA+ 验证了 S3、DynamoDB 等关键 AWS 服务中的算法。他们公开描述过一些 Bug，这些 Bug 几乎不可能通过测试发现，只会在并发操作的特定交错顺序下出现，而这种情况可能要经过数百万次执行才偶尔发生一次。
像 Raft 这样的共识协议，其 TLA+ 规格通常只有几百行。它描述了每一个合法的状态迁移、每一个不变式（例如‘每个任期内至多一个领导者’）以及每一条安全性属性。模型检验器随后会探索数十亿条可能的执行路径，验证没有任何一条路径违反任何不变式。这种规格确实接近代码，精确到你几乎可以机械地把它翻译成实现。
契约式设计
Bertrand Meyer 提出的契约式设计（Design by Contract，DbC）处在一个务实的中间地带。每个函数都规定前置条件（调用之前必须成立的条件）、后置条件（函数返回时保证成立的条件）以及不变式（对象在任何时候都必须成立的条件）。这些契约在开发阶段于运行时检查，在生产环境中则可以出于性能考虑选择关闭。
def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount转账的守恒后置条件，即转账前后总金额保持不变，正是那种单元测试很少覆盖、却能抓住 Bug 的不变式。它规定了系统的一条基本性质（钱既不会凭空产生，也不会凭空消失），任何正确的实现都必须满足它。
实用建议
完整的形式化规格对大多数软件而言并不现实。但你可以借助能融入常规开发流程的技术，显著缩小规格缺口。
- 充分利用类型系统。尽可能把约束编码进类型。当列表不应为空时，优先使用
NonEmptyList而不是List。即使UserId和OrderId都是字符串，也可以用 newtype 包装加以区分。你在类型中编码的每一条约束，都是编译器免费帮你检查的约束。 - 为核心逻辑编写基于属性的测试。找出系统应当维持的不变式，并将其表达为属性测试。哪怕只是几条精心挑选的属性，也能抓住成千上万个基于示例的测试所遗漏的 Bug。
- 明确边界的规格。最重要的规格位于系统边界：API 契约、数据库 schema、消息格式。使用 OpenAPI 规范、Protocol Buffers 或 JSON Schema，让这些内容可以被机器检查。
- 对关键并发系统使用 TLA+ 或 Alloy。如果你在设计共识算法、分布式锁或金融交易系统，相比生产环境中那些隐蔽的正确性 Bug 可能带来的代价，形式化规格的成本其实很小。
- 先写规格，再写测试。如果你无法精确描述正确的行为是什么样的，就无法验证它。花 30 分钟把函数应有的行为（包括所有情况和边界情况）写清楚，往往能在写下第一行代码之前就暴露设计问题。
‘足够详细的规格就是代码’这个说法并不完全正确，更准确的说法是：足够详细的规格会压缩 Bug 的生存空间。规格与实现之间的缝隙是歧义的栖身之所，而歧义正是 Bug 滋生的温床。每一种缩小这道缝隙的手段，无论是类型、属性、契约还是形式化方法，都能让软件更加正确。不是因为它们能阻止编码失误，而是因为它们能阻止编码失误往往所源于的规格失误。
