バグゼロを要求する上司が知らない『不可能性定理』

詳しく解説！雑学のコーナー

ソフトウェアの完全性に関する不可能性は、計算理論の根本的な限界から生じます。1936年、アラン・チューリングは「停止問題」を提示し、プログラムが停止するかどうかを判定する汎用的なアルゴリズムは存在しないことを証明しました。これは、バグの完全な検出が理論的に不可能であることを意味します。 チューリングの証明は、対角線論法を用いた美しいものでした。もし、あらゆるプログラムの停止を判定できるプログラムHが存在すると仮定します。そして、Hの判定結果と逆の動作をするプログラムPを作ります。PをH自身に適用すると矛盾が生じます。この自己言及的なパラドックスにより、完全な検証ツールの不存在が証明されたのです。 ライスの定理はさらに厳しい制約を示します。「プログラムの非自明な性質は、すべて決定不能である」。つまり、「このプログラムはクラッシュしない」「メモリリークがない」「仕様を満たす」といった、実用的に重要な性質のほとんどは、機械的に判定できないのです。 実践的な例として、NASAの事例があります。スペースシャトルのソフトウェアは、人類史上最も厳密にテストされたプログラムの一つです。42万行のコードに対し、開発費の40%以上がテストに費やされました。それでも、運用期間中に発見されたバグは0ではありませんでした。最後のバージョンでも、100万行あたり0.004個のバグが残存していたと報告されています。 マイクロソフトの研究は衝撃的です。Windows 10の開発において、テストカバレッジを70%から85%に上げるのに要したコストは、0%から70%にするコストの3倍でした。さらに85%から95%は10倍のコスト。そして、95%から99%は実質的に不可能と判断されました。限界費用が指数関数的に増大するのです。 Dijkstraの有名な言葉「テストは、バグの存在を示すことはできても、バグの不在を証明することはできない」は、この問題の本質を突いています。1兆回テストしても、1兆1回目にバグが出る可能性は否定できません。特に、並行処理やネットワーク関連のバグは、再現性が低く、検出が極めて困難です。 形式手法による証明も限界があります。CompCertのような検証済みコンパイラでさえ、証明の前提条件（ハードウェアの正しさ、OSの正しさ）に依存します。また、仕様自体が間違っている可能性は排除できません。Ariane 5ロケットの爆発事故は、仕様は満たしていたが、仕様自体が不適切だった例です。 「バグ密度」という現実的な指標があります。業界平均は、リリース時点で1000行あたり1-25個のバグです。優秀とされるプロジェクトでも0.1個/1000行。トヨタの車載ソフトウェアは0.02個/1000行という驚異的な品質ですが、それでもゼロではありません。1000万行のシステムなら、200個のバグが潜んでいる計算です。 カオスエンジニアリングは、バグの不可避性を前提とした新しいアプローチです。Netflixの「Chaos Monkey」は、本番環境でランダムにサーバーを停止させ、システムの耐障害性をテストします。「バグは必ず存在する」という前提で、その影響を最小化する設計を目指すのです。 最新の研究では、量子コンピューティングでも状況は改善しないことが分かっています。量子アルゴリズムの検証は、古典的アルゴリズムよりさらに困難です。AIによる自動バグ修正も研究されていますが、AIが生成したコードの正しさを誰が保証するのかという、新たな問題を生んでいます。