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 將其作為standard benchmark。

為什麼不執行自己的程式碼反而產生更少的 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 萬行零缺陷增量是可以實現的。只是它所需的遠見，超出了大多數組織願意付出的代價。