你的模块有三层。你可能只写了一层。

大多数 Bug 藏在”应该做什么”和”实际做什么”之间的缝隙里

你先写代码，再写测试，然后发现代码是错的。这是标准循环。也是为什么调试会消耗大多数项目时间线的一半。

Box Structure 把这个过程反转。你在写代码之前就定义行为，用数学方式验证这个定义，然后一层一层翻译成代码。结果是”构造即正确”的模块，而不是”测试碰巧通过所以正确”。

听起来不可能，直到你看到每一层有多小。

什么是 Box Structure？

Box Structure 在三个抽象层级上描述软件模块，每一层都是前一层的严格精化：

Black Box： 什么 Stimulus 产生什么 Response？没有 State，没有实现，只是一个从 History 到 Output 的 Pure Function。
State Box： 模块记住什么 State，每个 Stimulus 如何转换这个 State 并产生 Response？
Clear Box： 实际代码。

你由外向内设计。Black Box 是 Contract。State Box 是 Data Model。Clear Box 是代码。每一步都要先证明下层满足上层，才能继续。

这不是事后文档。Black Box 和 State Box 是 Formal Specification。它们就是 Design。代码排在最后。

Black Box：History 决定一切

Black Box 用 Stimulus History 和 Response 来定义模块。任何 Stimulus 的 Response 都取决于之前每一个 Stimulus。

考虑一个简单的 Token Bucket Rate Limiter。Black Box Specification 如下：

Stimulus	Condition on History	Response
`request(n)`	tokens available >= n	`grant(n)`
`request(n)`	tokens available < n	`deny`
`add_tokens(k)`	any history	no response, update history

Black Box 不说明 Token 如何被追踪。它只说：给定这段 Stimulus History，这是要求的 Response。

你可以在没有任何代码之前就验证这一点。写出 Stimulus 序列，手工计算预期 Response，检查 Specification 是否正确。不需要 Compiler，不需要 Test Runner，只需要逻辑。

State Box：增加记忆而不增加假设

State Box 通过引入一个 State 变量来精化 Black Box，使 History 成为隐式的。模块不再携带完整的 Stimulus History，而是记住一个压缩后的表示。

对于 Rate Limiter，State Box 引入了 tokens，即当前可用 Token 数量。Specification 变为：

Stimulus	Precondition on State	Response	New State
`request(n)`	`tokens >= n`	`grant(n)`	`tokens - n`
`request(n)`	`tokens < n`	`deny`	`tokens` (unchanged)
`add_tokens(k)`	any	no response	`tokens + k`

关键步骤是证明这个 State Box 与 Black Box 等价。State 变量 tokens 必须忠实地表示相关 History。如果应用 Black Box 规则产生的 Response 与 State Box Counter 相同，则 Refinement 有效。

这个证明通常很短。你验证的是一页 Specification，不是千行 Codebase。

Clear Box：不会给你惊喜的代码

Clear Box 是实现。它用没有 Goto、没有隐藏 Control Flow 的结构化语言写成。每个 Clear Box 都由 Sequence、Alternation（if-then-else）和 Iteration（while、for）构建。

以下是 Python 中的 Clear Box Implementation：

class TokenBucket:
    def __init__(self, capacity: int, refill_rate: float):
        self.capacity = capacity
        self.tokens = capacity
        self.refill_rate = refill_rate
        self.last_refill = time.monotonic()

    def _refill(self) -> None:
        now = time.monotonic()
        elapsed = now - self.last_refill
        added = int(elapsed * self.refill_rate)
        if added > 0:
            self.tokens = min(self.capacity, self.tokens + added)
            self.last_refill = now

    def request(self, n: int) -> str:
        self._refill()
        if self.tokens >= n:
            self.tokens -= n
            return f"grant({n})"
        return "deny"

    def add_tokens(self, k: int) -> None:
        self.tokens = min(self.capacity, self.tokens + k)

注意 _refill 不在 State Box 中。时间在 Black Box 和 State Box 里不存在。这些模型假设调用 add_tokens 时 Token 会神奇地出现。Clear Box 必须弥合这个差距。

大多数 Bug 就藏在这里。State Box 说 tokens 增加 k。Clear Box 还必须处理 Continuous Refill 和 Capacity Cap，同时仍然符合 State Box。

Cleanroom 如何在不运行测试的情况下证明正确性

在 Cleanroom 中，你不为 Clear Box 写 Unit Test。你执行 Verification。

对于每个 Control Structure，你写一个 Predicate，它必须在执行前后成立。对于 Sequence S1; S2，你证明 S1 的 Postcondition 蕴含 S2 的 Precondition。对于 if-then-else，你证明两个 Branch 都满足整体 Postcondition。对于 while 循环，你找到一个 Invariant，证明它在 Entry 时成立、每次 Iteration 保持、并在循环终止时蕴含期望的 Postcondition。

这不是 Proof Assistant。这是纸和笔。如果你曾经非正式地论证过一个递归 Function 会终止，你已经完成了 Cleanroom Proof 的百分之九十。

为什么大多数团队不用这个

显而易见的反对意见是时间。写 Black Box、State Box 和手写 Proof 听起来比直接写代码再修 Bug 更慢。

在 IBM 开发 Cleanroom 的 Harlan Mills 测量了相反的结果。Cleanroom 团队交付的代码缺陷比对照团队少一个数量级，总开发时间更短，因为他们几乎不花时间调试。

不那么明显的反对意见是文化。Box Structure 强迫你在打字之前先思考。大多数开发者觉得不舒服。Specification 感觉像官僚主义。它不是。它就是 Design。在 Cleanroom 中，Design 用足够精确、可以验证的记号书写，而不是那种第一张实现草稿就无视的图表。

Box Structure 值得付出开销的场景

你不需要用这种方式指定每个 Utility Function。Box Structure 在 Bug 成本高于写 Specification 时间的地方发光：Payment Processing、Authorization、Distributed Consensus、Protocol 和 Workflow Engine。它们也帮助那些反复将同一类 Bug 发到生产环境、却从不在测试中捕获的团队。

轻量起步方式

你不需要采用完整的 Cleanroom 流程。把 Box Structure 的想法借给一个模块。

选一个曾在生产环境引发问题的 Function。写出它的 Black Box：Input、Condition 和 Expected Output 的表格。不要看现有代码。写它应该做什么，而不是它实际做什么。

然后写 State Box。它需要什么 State？每个 Input 如何转换这个 State？与你的实现对比。有差异的地方，你就发现了一个 Bug 或一个未记录的 Assumption。

以下是 Python 的最小 Template，你可以适配：

"""
Black Box Specification: Rate Limiter

Stimuli: request(n), add_tokens(k)
History: sequence of all stimuli received

Rules:
  1. After any sequence of stimuli, tokens available =
     sum(add_tokens.k) - sum(grant.n)
  2. request(n) grants iff tokens available >= n
  3. tokens available never exceeds capacity

State Box Refinement:
  State: tokens (integer, 0 <= tokens <= capacity)
  Invariant: tokens accurately represents available tokens
"""

class TokenBucket:
    """Clear box implementation of the rate limiter state box."""

    def __init__(self, capacity: int):
        self.capacity = capacity
        self.tokens = capacity

    def request(self, n: int) -> str:
        if n <= 0:
            raise ValueError("request must be positive")
        if self.tokens >= n:
            self.tokens -= n
            return f"grant({n})"
        return "deny"

    def add_tokens(self, k: int) -> None:
        if k < 0:
            raise ValueError("cannot add negative tokens")
        self.tokens = min(self.capacity, self.tokens + k)

Comment 就是 Specification。Code 就是 Implementation。把它们放在同一个文件里，让 Refinement 可见且可 Review。

真正的价值在于关注点分离

Box Structure 不是魔法。它不会抓住每一个 Bug。它做的是强制一种大多数开发流程都跳过的纪律：在构建之前定义”正确”意味着什么。

Black Box 把模块的 Contract 和内部实现分离。State Box 把 Data Model 和代码分离。Clear Box 把 Implementation 和 Proof 分离。每一层只有一个职责，你在进入下一层之前验证它。

这就是你应该关心的原因。“应该做什么”和”实际做什么”之间的缝隙是你的 Bug 的栖息地，而 Box Structure 是在你写任何一个 Test 之前就系统性地关闭这个缝隙的方法。

如果你想深入了解，Mills 的《Cleanroom Software Engineering》和原始 IBM Technical Report 仍然是最清晰的参考资料。这些想法很老。它们阻止的 Bug 并不老。