仕様と実装のギャップにこそバグが潜む
ほとんどのバグは、仕様が記述する内容と実際のコードの動作のあいだにあるギャップに潜んでいます。形式的仕様がそのギャップをどう狭めるかを解説します。
James Whitfield
この主張は、プログラミング言語理論の界隈で時折話題に上がります。「十分に詳細な仕様は、コードと区別がつかない」というものです。ここに含まれる意図は挑発的です。プログラムが何をすべきかを記述することと、実際にそれを行うことのあいだの境界線は、我々が思っているよりずっと薄いのだと言っているのです。仕様が曖昧さを完全に取り除けるほど精密であれば、それは実質的にプログラムを書き終えているのと同じです。
これは単なる哲学論争ではありません。ソフトウェアの作り方、仕様が果たす役割、そしてほとんどのバグがコーディングミスではなく仕様の隙間から生まれる理由に、実践的な意味があります。仕様がどこで終わり、実装がどこから始まるのかを理解すると、テスト、型、そして正しさについての考え方が変わるはずです。
ほとんどのバグはどこから来るのか
バグの原因を開発者に聞けば、たいてい「コード」と答えるでしょう。しかし、ソフトウェアの欠陥を調べた多くの研究が示すのは、別の事実です。ほとんどのバグは、意図と実装のあいだのギャップから生まれています。コードは開発者が指示したとおりに正しく動いています。ただ、その指示が間違っていたのです。仕様（形式的であれ非形式的であれ）が曖昧だったり、不完全だったり、誤解されたりしていたからです。
典型的な例を挙げましょう。仕様に「システムは同時リクエストを処理しなければならない」とあったとします。「処理する」とはどういう意味でしょうか。順番に処理するのか、同時に処理するのか。多すぎる場合はキューに入れるのか。「多すぎる」とはどのくらいなのか。キューが満杯のときに到着したリクエストはどうなるのか。これらは実装の細部ではなく、仕様の穴です。答えられていない問いはひとつずつ潜在的なバグになります。開発者は実装を通じて暗黙のうちに答えを出しますが、その答えがユーザーや他の開発者の期待と一致する保証はないからです。
仕様の精密さのスペクトラム
仕様は非形式的なものから形式的なものまで、スペクトラム上に存在します。
- 自然言語。 「ログインシステムは安全で使いやすくあるべきだ」。これは仕様というより願望に近いものです。どの単語も曖昧です。「安全」とは何か。「使いやすい」とは何か。要件の形をした判断の先送りにすぎません。
- 構造化された自然言語。 「ユーザーが10分以内に3回連続でパスワードを誤入力したら、アカウントを30分間ロックする」。より精密になりましたが、まだ曖昧さが残ります。「パスワードの誤入力」には空の送信も含まれるのか。3回の試行は連続している必要があるのか。10分の時間枠はスライディングか固定か。
- 型シグネチャ。
authenticate(username: string, password: string) -> Result<User, AuthError>。関数のインターフェースは正確に定義されていますが、振る舞いについては何も語りません。入力と出力の形はわかっても、両者の関係はわからないのです。 - プロパティベースの仕様。 「データベース内のすべての有効なユーザー名とパスワードの組に対して、
authenticateはuser.username == usernameを満たすOk(user)を返す」。論理的な量化子を使うことで、振る舞いをより精密に制約できます。 - 形式仕様。 システムの振る舞いを完全に数学的にモデル化したものです。すべての状態、すべての遷移、すべての不変条件を記述します。このレベルになると、仕様と実装はほぼ同じものになります。
形式仕様に近づくほど曖昧さの入る余地は減り、バグの入る余地も減ります。ただし、一歩進むごとに労力と専門的なスキルも増えます。実践的な問いは、与えられたプロジェクトでこのスペクトラムをどこまで進むべきか、ということです。
軽量な仕様としての型
型システムは、日常のプログラミングで最も広く使われている仕様の形式です。振る舞いを記述するわけではありませんが、振る舞いを制約します。UserではなくOption<User>を返す関数は、ユーザーが見つからない可能性があることを仕様として示しており、コンパイラはすべての呼び出し側にその可能性を処理させます。
// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User // What if ID is invalid?
// // What if user not found?
// // Does it panic? Return null?
// // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.Rust、Haskell、TypeScriptといった言語は、形式手法の訓練を受けていなくても、表現力の高い型システムが仕様の隙間をどれだけ狭められるかを示しています。代数的データ型、ジェネリクスの制約、網羅的なパターンマッチングを組み合わせると、型レベルでプログラムの振る舞いの多くを規定でき、その検証はコンパイラが自動で行ってくれます。
重要な考え方は、型の注釈はすべて自動的に検査される仕様である、ということです。型システムで符号化できる振る舞いひとつひとつが、将来発生しなくなるバグの一類型に相当します。
プロパティベーステスト：振る舞いを仕様化する
ユニットテストは、例に基づく仕様です。「この特定の入力に対しては、この特定の出力を期待する」というものです。有用ではありますが、本質的に不完全です。自分が思いついたケースしかテストできないからです。プロパティベーステストはこれを逆転させます。すべての入力に対して成り立つべきプロパティを指定し、テストフレームワークがランダムな入力を生成して違反を探します。
from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.このテストにある3つのプロパティは、単にソートをテストしているだけではありません。ソートを定義しているのです。3つのプロパティすべてを満たす関数は、定義上、正しいソートです。これは「仕様としてのコード」という考え方を最も実践的な形で表したものです。正しい振る舞いを定義するプロパティを書き、あとはテストフレームワークに実装がそれを満たすか検証させるのです。
TLA+とモデル検査
分散システム、金融プラットフォーム、重要なインフラのように、バグのコストが高いシステムでは、TLA+のような形式仕様ツールがより強い保証を与えてくれます。TLA+（Temporal Logic of Actions）では、システムの振る舞いを状態機械として記述し、モデル検査にかけられます。すなわち、考えうるすべての実行パスを網羅的に探索し、不変条件が成り立つことを検証するのです。
Amazonは、S3、DynamoDBなどAWSの重要なサービスのアルゴリズムの検証にTLA+を使ってきました。テストではほぼ見つけられなかったであろうバグを発見したことを公表しています。並行処理の特定のインターリーブでしか現れず、数百万回の実行に一度しか起きないような種類のバグです。
Raftのような合意プロトコルのTLA+仕様は、通常数百行程度です。合法なすべての状態遷移、すべての不変条件（例：「任期ごとにリーダーは高々1人」）、すべての安全性プロパティを記述します。モデル検査器は何十億もの実行パスを探索し、どのパスも不変条件に違反しないことを検証します。これは実際のコードに非常に近い仕様であり、機械的に実装へ変換できるほど精密です。
契約による設計
Bertrand Meyerの契約による設計（Design by Contract, DbC）は、実用的な中間地点に位置します。各関数について、事前条件（関数の呼び出し前に真でなければならないこと）、事後条件（関数が返るときに保証されること）、そしてインバリアント（オブジェクトについて常に真でなければならないこと）を指定します。これらの契約は開発中に実行時にチェックされ、性能のために本番環境では任意で無効化できます。
def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount資金移動の前後で総額が変わらないという事後条件、すなわち保存則は、ユニットテストではめったにカバーされないバグを捕まえるタイプの不変条件です。お金は作られも消えもしない、というシステムの基本的な性質を規定しており、正しい実装はすべてこれを満たさなければなりません。
実践的な推奨事項
形式仕様の全面的な適用は、ほとんどのソフトウェアにとって現実的ではありません。しかし、通常の開発ワークフローに収まる手法を使えば、仕様のギャップをかなり狭めることができます。
- 型システムを積極的に使う。 可能な限り制約を型として表現しましょう。リストが空であってはならない場合は、
ListよりもNonEmptyListを選びます。両方とも文字列であっても、newtypeラッパーでUserIdとOrderIdを区別しましょう。型で表現した制約は、コンパイラがタダで検査してくれる制約になります。 - コアロジックにはプロパティベーステストを書く。 システムが維持すべき不変条件を特定し、プロパティテストとして表現しましょう。厳選された数個のプロパティでも、何千もの例ベースのテストが見逃すバグを捕まえられます。
- 境界を仕様化する。 最も重要な仕様はシステムの境界にあります。APIの契約、データベーススキーマ、メッセージフォーマットです。OpenAPI、Protocol Buffers、JSON Schemaを使って、機械的に検査できるようにしましょう。
- 重要な並行システムにはTLA+やAlloyを使う。 合意アルゴリズム、分散ロック、金融トランザクションシステムを設計しているなら、形式仕様のコストは、本番環境で発生する微妙な正しさのバグのコストに比べれば小さいものです。
- テストより先に仕様を書く。 正しい振る舞いを正確に述べられないなら、それを検証することもできません。関数が何をすべきかを（エッジケースを含むすべてのケースについて）明確に書き出すのに30分かけると、コードを1行書く前に設計上の問題が見つかることがよくあります。
「十分に詳細な仕様はコードである」という主張は、正確とは言えません。より正確に言えば、十分に詳細な仕様はバグの入る余地を取り除く、ということです。仕様と実装のあいだのギャップには曖昧さが潜み、曖昧さこそがバグを生む温床です。型、プロパティ、契約、形式手法など、そのギャップを狭める手法はどれもソフトウェアをより正しくします。コーディングミスを防いでくれるからではなく、コーディングミスの多くの原因である仕様のミスを防いでくれるからです。
