1980 年代软件行业的平均水平是每千行代码 30 到 60 个缺陷。IBM 的 Cleanroom 团队交付了一个 2 万行的编译器增量,在测试中发现了 53 个缺陷。也就是每 KLOC 2.6 个。一些 1 万行的独立增量在进入系统测试时,没有发现任何缺陷。

最离奇的部分?程序员被禁止运行自己的代码。

Cleanroom software engineering 到底是什么意思

Cleanroom software engineering 由数学家 Harlan Mills 于 1980 年代在 IBM 开发,是一种基于理论的流程,依赖 formal specification、structured design 和 mathematical correctness verification,而不是单元测试和调试。这个名字来自半导体制造。在芯片工厂里,你不会先引入灰尘再把它擦掉。你要从一开始就防止污染。

在 Cleanroom 中,开发人员不做单元测试。他们不调试。他们验证。

该流程将软件划分为增量,通常为 5000 到 15000 行代码。每个增量都要经过规格说明、设计、验证,然后作为一个完整的单元进行统计测试。开发人员编写代码,但在开发过程中不允许编译或执行。代码第一次运行是在正式系统测试期间。

box structure verification 如何取代调试

核心机制是 box structure specification。每个组件在三个层次上定义。

black box 规定了外部行为。它定义了刺激和响应,而不提及内部状态。

state box 添加了内部状态变量和状态转换函数。

clear box 是实际的实现,必须是 state box 的结构化细化。

这种层级很重要,因为它让你可以在每个层次上独立验证正确性。你证明 state box 实现了 black box,而 clear box 实现了 state box。

下面是实际应用中,一个具有非平凡正确性论证的函数的样子:

from typing import Optional

def binary_search(arr: list[int], target: int) -> Optional[int]:
    """
    Black box spec:
      Pre:  arr is sorted in non-decreasing order.
      Post: Returns index i such that arr[i] == target,
            or None if target is not present.
    """
    low, high = 0, len(arr) - 1

    while low <= high:
        mid = (low + high) // 2

        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            low = mid + 1
        else:
            high = mid - 1

    return None

循环的 verification argument 才是重点。团队一起审查并确认三个事实。第一,如果 arr[mid] == target,则 postcondition 立即满足。第二,如果 arr[mid] < target,则目标只能存在于大于 mid 的索引处,因此设置 low = mid + 1 可以保持目标在 arr[low:high+1] 中的不变性,前提是该目标确实存在。第三,如果 arr[mid] > target,则对称论证对 high = mid - 1 成立。

这不是有人在代码评审中问你有没有想过空数组的情况。这是一个结构化的小组证明,证明每一个可能的输入都会产生指定的输出。

IBM 零缺陷主张背后的数据

IBM 在 1980 年代末和 1990 年代初将 Cleanroom 应用于三个重大项目:COBOL Structuring Facility(4 万行)、空军直升机飞行程序(3.5 万行)和 NASA 航天运输规划系统(4.5 万行)。

COBOL/SF 的数据最为详细。第一个 2 万行的增量采用 formal specifications、box structure design 和小组 correctness verification 进行开发。开发人员在开发过程中不得编译或运行自己的模块。代码直接进入系统测试。

结果:测试中发现 53 个缺陷。超过 90% 的缺陷在代码执行之前的验证阶段就被捕获了。

作为对比,当时 IBM 的传统项目大约有 60% 的缺陷在执行前被发现。Cleanroom 扭转了这个比例。

一些增量,特别是 1 万行以下的小型增量,在系统测试中报告零缺陷。这就是”1 万行零缺陷”说法的来源。它确实发生了。并非普遍如此,但重现性足够高,以至于 IBM 将其作为标准基准。

为什么不运行自己的代码反而产生更少的 bug

这是让开发人员大脑宕机的部分。不测试怎么能产生更好的代码?

答案是认知层面的,而不是技术层面的。当你知道自己不能运行代码来检查工作时,你会更仔细地设计。你写更小的函数。你在打字之前就想好边界情况。你依赖类型系统和结构化编程,因为你没有安全网。

这和外科医生使用清单的原因是一样的。这种约束迫使你进入不同的心智模式。

还有一层统计质量控制。Cleanroom 使用基于 operational profile 的 statistical usage testing。测试用例是从实际用户行为的概率分布中提取的,而不是开发人员猜测 bug 在哪里。这意味着你在衡量可靠性,而不仅仅是猎杀 bug。

让 Cleanroom 保持小众的权衡

Cleanroom 没有统治世界。有原因的。

首先,培训门槛很高。你需要能够编写 formal specifications 并构建 mathematical correctness arguments 的团队。2025 年的大多数 CS 毕业生从未对非平凡函数进行过形式化证明。

其次,前期设计成本很高。IBM 报告称,在 COBOL/SF 项目中,specification 文本以四比一的比例超过设计文本。你在用设计时间换取测试时间。这对编译器和飞行软件有效。对每周需求都要变化的 CRUD 应用无效。

第三,零缺陷主张指的是缺陷密度,而不是完全没有 bug。一个 Cleanroom 增量仍然可能存在 specification errors。如果 black box 错了,那么经过验证的 clear box 也是错的,只是按构造方式而言。

如何在不搞官僚主义的情况下偷走 Cleanroom 的纪律

你可能无法采用完整的 Cleanroom。你的产品经理不会等待四比一的规格代码比。但你可以偷走高价值的部分。

1. 在实现之前先写 contract。

使用 preconditions、postconditions 和 invariants 来定义你的 black box。即使是非正式的注释也会迫使你在优化之前考虑边界。

from typing import List, Tuple

def partition(nums: List[int], pivot: int) -> Tuple[List[int], List[int]]:
    """
    Black box spec:
      Pre:  True (any list of integers is valid).
      Post: left contains exactly the elements of nums where x <= pivot.
            right contains exactly the elements of nums where x > pivot.
            len(left) + len(right) == len(nums).
    """
    left = [x for x in nums if x <= pivot]
    right = [x for x in nums if x > pivot]

    # Runtime checks act as lightweight verification witnesses.
    assert all(x <= pivot for x in left)
    assert all(x > pivot for x in right)
    assert len(left) + len(right) == len(nums)

    return left, right

2. 用一些 verification arguments 替代单元测试。

在写测试之前,先写一句关于代码为什么正确的论证。如果你构造不出这句话,说明设计太复杂了。这是现代团队最有效的 Cleanroom 实践。

3. 使用 property-based testing 作为 statistical usage testing。

Python 中的 Hypothesis 或 JavaScript 中的 fast-check 等工具从分布中生成输入。这在精神上更接近 Cleanroom 的 statistical testing,而不是基于示例的单元测试。

4. 把编译和验证分开。

如果你习惯性地写一行、编译、改错别字、再写一行,那你就是在用抽搐反射调试。试着在运行之前写出一个完整的逻辑单元。不适感才是重点。

常见问题

Cleanroom 今天还在用吗?

它在安全关键和任务关键领域存活了下来。NASA、FAA 和一些医疗设备制造商使用该流程的变体。在商业软件中很少见。

我真的可以在没有单元测试的情况下交付代码吗?

只有当你用同样严格的东西来替代它时才行。Cleanroom 团队在验证上花费的时间比大多数团队在测试上花费的时间还要多。时间没有消失。它只是向左移动了。

Cleanroom 能保证零 bug 吗?

不能。它保证实现与 specification 高度一致。如果 specification 错了,bug 会被完美地保留下来。

对生产力有什么影响?

IBM 报告称,在 COBOL/SF 项目上,生产力超过每人每月 400 行代码,主要是因为大幅减少的测试时间抵消了增加的设计工作量。

底线

下次有人声称某种方法论能交付零缺陷软件时,问他要项目数据。IBM 的 Cleanroom 数字是真实的,但它们来自特定的背景:经验丰富的团队、正式培训、增量交付,以及愿意验证而不是调试。

1 万行零缺陷增量是可以实现的。只是它所需的远见,超出了大多数组织愿意付出的代价。