你的模組有三層。你可能只寫了一層。

大多數 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 並不老。