ほとんどのバグは「あるべき姿」と「実際の動作」の間に潜んでいる
まずコードを書き、次にテストを書き、そしてコードが間違っていたことに気づく。これが標準的なループだ。だからデバッグは、ほとんどのプロジェクトのタイムラインの半分を消費する。
Box Structureはこれを反転させる。コードを書く前に振る舞いを定義し、その定義を数学的に検証してから、1層ずつコードに翻訳する。その結果、テストがたまたま通ったから正しいのではなく、構造的に正しいモジュールができる。
各層がどれほど小さいかを見るまで、これは不可能に聞こえる。
Box Structureとは何か
Box Structureは、ソフトウェアモジュールを3つの抽象レベルで記述する。それぞれは前の層の厳密な精緻化である。
- Black Box: どのStimulusがどのResponseを生み出すか？Stateも実装もない。HistoryからOutputへの純粋な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は、Historyを暗黙的にするState変数を導入することでBlack Boxを精緻化する。Stimulusの完全なHistoryを持ち歩くのではなく、モジュールは圧縮された表現を記憶する。
Rate Limiterの場合、State Boxは現在利用可能なToken数であるtokensを導入する。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のルールを適用した結果がState BoxのCounterと同じResponseを生み出せば、そのRefinementは有効だ。
この証明は通常短い。検証するのは1ページの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がその差を埋めなければならない。
ここにほとんどのバグが潜んでいる。State Boxではtokensがk増えると述べている。Clear Boxは、継続的なRefillやCapacity Capも扱いながら、State Boxに準拠し続けなければならない。
Cleanroomがテストを走らせずに正しさを証明する方法
Cleanroomでは、Clear Boxに対するUnit Testを書かない。代わりにVerificationを行う。
各Control Structureに対して、実行前後に成り立たなければならないPredicateを書く。SequenceS1; S2では、S1のPostconditionがS2のPreconditionを含意することを証明する。if-then-elseでは、両方のBranchが全体のPostconditionを満たすことを証明する。whileループでは、Invariantを見つけ、それがEntry時に成り立ち、各Iterationで保持され、ループ終了時に望ましいPostconditionを含意することを証明する。
これはProof Assistantではない。紙と鉛筆だ。再帰的なFunctionが停止することを非形式的に論じたことがあれば、すでにCleanroomの証明の90パーセントを行っているのだ。
なぜほとんどのチームがこれを使わないのか
明白な反論は時間だ。Black BoxとState Boxと手書きの証明を書くのは、コードを書いてバグを修正するより遅いように聞こえる。
IBMでCleanroomを開発したHarlan Millsは、逆を測定した。Cleanroomチームは対照チームよりも1桁少ない欠陥でコードを納品し、総開発時間はデバッガでほとんど時間を費やさなかったため短かった。
もう少し見えにくい反論は文化的なものだ。Box Structureは、タイプする前に考えることを強制する。ほとんどの開発者はこれを不快に感じる。Specificationは官僚主義のように感じられる。違う。それはDesignだ。Cleanroomでは、Designは検証に十分な精度を持った記法で書かれ、最初の実装ドラフトに無視される図式ではない。
Box Structureのオーバーヘッドに見合う場面
すべてのUtility Functionをこの方法で指定する必要はない。Box Structureが輝くのは、バグのコストがSpecificationを書く時間を上回る場面だ。Payment Processing、Authorization、Distributed Consensus、Protocol、Workflow Engineなど。同じカテゴリのバグを繰り返しProductionに出荷し、テストでは絶対に検出できないチームにも役立つ。
手軽な始め方
Cleanroomプロセス全体を導入する必要はない。Box Structureのアイデアを1つのモジュールに借りる。
Productionで問題を引き起こしたFunctionを選ぶ。そのBlack Boxを書く。Input、Condition、Expected Outputのテーブルだ。既存のコードを見ないで。実際にやっていることではなく、あるべきことを書く。
次にState Boxを書く。どのStateが必要か？各InputがそのStateをどう変換するか？実装と比較しよう。違いがあれば、バグか文書化されていない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は魔法ではない。すべてのバグを捕まえるわけではない。それらが行うことは、ほとんどの開発プロセスが飛ばしてしまう規律を強制することだ。構築する前に「正しい」とは何かを定義する。
Black BoxはモジュールのContractと内部を分離する。State BoxはData ModelとCodeを分離する。Clear BoxはImplementationとProofを分離する。各層は1つの仕事を持ち、次に進む前に検証する。
だから気にするべきなのだ。「あるべき姿」と「実際の動作」の間の隙間が、バグの住処であり、Box Structureは、1つのテストも書く前にその隙間を閉じる体系的な方法なのだ。
さらに深く知りたいなら、Millsの『Cleanroom Software Engineering』とオリジナルのIBM Technical Reportが、未だに最も明確な参考文献だ。アイデアは古い。それが防ぐバグは、そうではない。