Cleanroom software engineering は 1,000 行あたり 0.1 の defect を達成する。業界平均は 10 から 50 だ。問題は、フルの Cleanroom ではチームを author と verifier に分割し、すべての module の前に formal specification を書き、developer が自分の code を実行することを、分離した test team が統計的に validate するまで禁止しなければならないことだ。

ほとんどの engineering manager はその process を見て、headcount で素早く計算し、quality が overhead に見合わないと判断する。半分正しい。フルの Cleanroom process は重い。しかし underlying principles は lightweight で、verification army を雇ったり cargo test を禁止したりしなくても導入できる。

Cleanroom とは実際に何か

Cleanroom は、1970 年代に IBM の Harlan Mills によって開発された software development process だ。名前は半導体製造に由来する: defect を生み出す条件を防ぎ、事後的に inspect して取り除くのではない。core claim は、code を書く前に bug が不可能になるほど慎重に設計すれば、software は construction によって correct になりうるというものだ。

method は 3 つの practice に基づく: statistical process control 下での incremental development、box structures による function-theoretic design、分離した team による statistical usage testing。この 3 つは相互依存している。1 つ壊すと、他は力を失う。

その相互依存性が overhead の myth の根源だ。team は 3 つすべてか無かだと仮定する。それは違う。practice は互いに補強するが、それぞれ単独でも value を生む。

overhead が実際に存在する場所

人々が恐れる 80% の overhead は、2 つの具体的な要件から来る。

第一に、no-execution rule だ。フルの Cleanroom では、code を書いた developer は compile も実行も unit test もしない。分離した verification team がすべての実行を扱う。これは developer にタイプする前にすべての case を推論させ、それがまさに code が初回で動く理由だ。しかしこれは engineering headcount を倍増させるか、既存の team を互いに恨み合う 2 つの group に分割する必要もある。

第二に、formal verification step だ。clear box implementation を書く前に、team は black box specification と state box refinement を書き、state box が black box と等価であることを手で証明する。これは pencil-and-paper proof であり、proof assistant ではない。機能するが、ほとんどの team が持たない時間と training を必要とする。

第三の practice、statistical process control による incremental development は、すでに sprint をやっていれば実質無料だ。小さな increment を ship し、increment ごとに defect density を測定し、increment が defect target を超えたら process を停止して method のどこが間違っていたかを突き止める。これは単に “done” のより厳格な定義を持つ data-driven retrospective に過ぎない。

pragmatism なサブセット: 構造は残し、官僚制は捨てる

構造的 discipline を保ち、組織的 mandate を捨てれば、Cleanroom の defect reduction の大半を得られる。

保つべきものはこうだ。

code の前に contract を書く。 Z notation での formal specification ではない。input、output、precondition、postcondition の明確な記述だけだ。correct が何を意味するか書けなければ、correct な code は書けない。

state machine を明示的に encode する。 ほとんどの bug は、developer が不可能だと仮定した state transition に潜む。logic を書く前に、state と transition を table や data structure で定義する。

誰か他の人に logic を test させる。 authorship と verification の分離は Cleanroom の最も強力な idea だ。分離した team は必要ない。code を書かなかった 1 人に test case を設計してもらえばいい。自分の code を test すると、自分の assumption を test していることになる。

increment ごとに defect density を測定する。 各 phase から何個の bug が漏れるか追跡する。integration bug が繰り返し漏れるなら、問題は careless な developer ではない。process が integration bug を存在させているのが問題だ。

捨てるべきものはこうだ。

no-execution rule を捨てる。 developer に自分の code を実行させる。先に推論する discipline は、その後に quick sanity check を許しても価値がある。point は compiler を走らせる前に考えることであって、compiler が存在しないふりをすることではない。

formal hand proof を捨てる。 avionics software を書いているのでなければ、pencil-and-paper proof は overkill だ。property-based tests と type-driven design で置き換える。これらは同じ推論の mechanized version であり、CI で動く。

statistical usage testing の要件を捨てる。 フルの Cleanroom は code coverage ではなく usage profile に対して test する。データがあれば素晴らしい。なければ、property-based testing と mutation testing で、既に使っている tools でほぼ同じ confidence が得られる。

Python における lightweight Cleanroom workflow

単一の module において、実際にどう見えるか。contract から始める。

"""
Black Box: Token Bucket Rate Limiter

Stimuli: request(n), add_tokens(k)
Precondition: n > 0, k >= 0, capacity > 0
Postcondition:
  - request(n) grants iff available tokens >= n
  - request(n) reduces available tokens by n if granted
  - add_tokens(k) increases available tokens by k, capped at capacity
  - available tokens never negative, never exceeds capacity
"""

次に state machine を encode する。

from enum import Enum, auto

class RateLimitState(Enum):
    READY = auto()      # tokens >= 1, requests may grant
    DEPLETED = auto()   # tokens == 0, requests deny

# Transitions depend on token count, not external events
# READY -> DEPLETED when tokens reach 0
# DEPLETED -> READY when tokens added above 0

次に implementation を書く。

import time
from dataclasses import dataclass

@dataclass
class TokenBucket:
    capacity: int
    tokens: int
    refill_rate: float
    last_refill: float

    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) -> bool:
        if n <= 0:
            raise ValueError("request must be positive")
        self._refill()
        if self.tokens >= n:
            self.tokens -= n
            return True
        return False

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

contract は docstring にある。state machine は明示的だ。implementation は短く、inspection で verifiable だ。これはフルの Cleanroom ではない。cowboy coding でもない。

実際に実行できる verification step

フルの Cleanroom では、分離した team が usage profile に基づいて statistical test を書く。pragmatic 版では、property-based tests を書き、同僚に review してもらう。

from hypothesis import given, strategies as st

@given(
    capacity=st.integers(min_value=1, max_value=1000),
    initial=st.integers(min_value=0, max_value=1000),
    requests=st.lists(st.integers(min_value=1, max_value=100), max_size=50),
)
def test_token_bucket_never_overdrafts(capacity, initial, requests):
    bucket = TokenBucket(
        capacity=capacity,
        tokens=min(initial, capacity),
        refill_rate=0.0,
        last_refill=time.monotonic(),
    )

    for n in requests:
        granted = bucket.request(n)
        assert bucket.tokens >= 0
        if granted:
            # tokens were deducted, so pre-request balance was sufficient
            pass
        else:
            # request denied, current tokens insufficient
            assert bucket.tokens < n

この test は特定の output を check しない。invariant を check する: bucket は持っている以上の token を決して grant しない。これは Cleanroom proof の property-based version だ。自動で動き、思いつかなかった edge case を見つけ、分離した verification team を必要としない。

trade-off は現実のものだ

pragmatic Cleanroom はタダではない。code の前に contract を書くには discipline が必要だ。explicit な state machine は、code が “自明” のとき boilerplate に感じられる。誰か他の人に logic を test させるには調整が必要だ。

本物ほど強力でもない。フル Cleanroom の no-execution rule は、REPL が 1 keystroke 先にあるときには再現できない深さの推論を強制する。formal proof は、properties が間違っていれば property-based tests が見逃すかもしれない logical error を捉える。

しかし比較対象は pragmatic Cleanroom 対 フル Cleanroom ではない。比較対象は pragmatic Cleanroom 対 今やっていることだ。今の process が 1KLOC あたり 20 defect を出し、pragmatic Cleanroom が 5 にしてくれるなら、それは overhead の一部で 4 倍の改善だ。

価値がある場面

すべての utility function にこれを使うな。bug が高くつく code に使え: authorization、billing、distributed protocol、3 つ以上の state を持つ state machine、production incident を 2 回以上引き起こしたもの。

これが必要な signal は complexity ではない。repeated surprise だ。team が test や production で同じ category の bug を繰り返し見つけるなら、問題は developer が careless だということではない。code の contract が定義されていなかったので “correct” が specified されていなかったのが問題だ。

1 つの module から始める

management の承認や process overhaul は必要ない。以前に被害を受けた 1 つの module を選ぶ。implementation に触れる前に docstring で contract を書く。state と transition を定義する。同僚に code を見ないで test を書いてもらう。CI で property-based tests を走らせる。

それだけだ。分離した team も、formal notation も、自分の code を実行する禁止もない。

Cleanroom の 1KLOC あたり 0.1 defect は magic ではなかった。人々に build する前に correct を定義させる process の output だった。その効果の大半は、docstring と state machine table と、code ではなく assumption を test してくれる同僚で得られる。