1. 正当性理論とは
プログラムの正当性理論とは、コンピュータプログラムがその仕様に従って正しく動作することを形式的に証明するための理論です。プログラムの信頼性を保証するためには、単にテストやデバッグを行うだけでなく、プログラムが設計された通りに動作することを数学的に証明する必要があります。この理論は、プログラムがその仕様に従って正しく動作することを保証するために非常に重要です。特に、重要なシステムや安全性が求められる環境においては、プログラムの正当性が保証されることが不可欠です。
2. 詳細説明
正当性理論には、部分正当性と全正当性という2つの主要な概念があります。
部分正当性
部分正当性とは、プログラムが正しい初期状態から開始し、その途中でエラーを起こさずに特定の結果を得ることができるという性質です。しかし、部分正当性だけでは、プログラムが必ず停止することは保証されません。部分正当性は、プログラムの途中までの正しさを示すものであり、プログラムが無限ループに陥るかどうかまではカバーしません。
数学的に表現すると、「前提条件Pが満たされた状態でプログラムが実行され、プログラムが終了した場合、事後条件Qが満たされる」ことを{P}program{Q}と表記します。これはホーア論理の基本的な考え方です。
全正当性
全正当性は、部分正当性に加えて、プログラムが必ず停止することも保証する性質です。全正当性が証明されたプログラムは、必ず正しい結果を生成し、無限ループに陥ることなく終了します。全正当性を証明するには、プログラムが特定の条件を満たした場合に確実に停止することを示すことが必要です。
全正当性は数学的に「前提条件Pが満たされた状態でプログラムを実行すると、必ずプログラムは終了し、終了時には事後条件Qが満たされる」と表現できます。
図1：部分正当性と全正当性の関係図
図2：ホーア論理による正当性証明の例
ホーア論理
プログラムの正当性を証明するための形式的な体系として、トニー・ホーア（C.A.R. Hoare）が1969年に提案したホーア論理があります。この論理体系では、プログラムの実行前の状態（前提条件）と実行後の状態（事後条件）を数学的に記述し、プログラムがこれらの条件を満たすことを証明します。
ホーア論理は「{P} C {Q}」という形式で表されます：
- P は前提条件（プログラム実行前に成り立つ条件）
- C はプログラムコード
- Q は事後条件（プログラム実行後に成り立つ条件）
この表記は「前提条件 P が成り立つ状態でプログラム C を実行すると、終了時には事後条件 Q が成り立つ」ことを意味します。例えば、「{x = 0} x := x + 1 {x = 1}」は、変数 x が 0 である状態でプログラムを実行すると、終了後には x が 1 になることを表しています。
ホーア論理では、ループ構造の正当性を証明するために「ループ不変式」という概念も重要です。ループ不変式とは、ループの各繰り返しの前後で常に成り立つ条件であり、これを用いてループを含むプログラムの部分正当性を証明できます。
停止問題
ここで、停止問題について触れておく必要があります。停止問題とは、与えられたプログラムと入力に対して、そのプログラムが停止するかどうかを決定する問題です。この問題は一般には解決不可能であることが知られており、すべてのプログラムに対して停止するかどうかを事前に判断することは不可能です。したがって、全正当性を証明することは、すべてのプログラムについては不可能であり、特定の条件下でのみ証明可能です。
チューリングが1936年に証明したこの不可能性は、コンピュータサイエンスの根幹を成す重要な理論です。これにより、プログラムの全正当性を自動的に証明するアルゴリズムは存在しえないことが分かります。代わりに、特定のプログラムパターンや制約された条件下での証明手法が研究されています。
図3：停止問題の説明図
3. 応用例
図4：プログラム正当性の検証レベル一覧表
プログラムの正当性理論は、特に以下のような状況で重要な役割を果たします。
- 航空宇宙産業: 航空機や宇宙船の制御システムは、極めて高い安全性が要求されます。これらのシステムのプログラムが正しく動作しない場合、重大な事故が発生する可能性があります。したがって、これらのプログラムには全正当性が求められます。
- 金融システム: 金融取引を扱うシステムでは、取引データの正確性が非常に重要です。プログラムの正当性が保証されることで、不正確な取引やデータの損失を防ぐことができます。
- 医療機器: 医療機器の制御プログラムもまた、正当性が保証されることが求められます。これにより、誤作動による患者への危害を防ぐことができます。
- 形式検証ツール: 形式検証ツール（例：Coq、Isabelle、TLA+など）は、プログラムの正当性を証明するために使用されます。これらのツールを使用することで、特定の性質が満たされているかを数学的に検証できます。
- スマートコントラクト: ブロックチェーン上のスマートコントラクトは、一度デプロイされると変更できないため、事前に正当性を証明することが極めて重要です。DAO事件のような大規模な問題を防ぐために、形式検証が活用されています。
4. 練習問題
学習者が理解を深めるための練習問題をいくつか提示します。
問題1: 以下のプログラムが与えられたとき、部分正当性と全正当性の観点からその正当性を証明しなさい。
x := 0;
while x < 5 do
x := x + 1;
end while;解答例
- 部分正当性: このプログラムの前提条件を「true」（任意の状態から開始可能）、事後条件を「x ≥ 5」とすると、ループが終了するときには必ず x = 5 となり、事後条件を満たします。よって部分正当性は証明されます。
- 全正当性: 各ループの繰り返しで x の値は1ずつ増加し、x < 5 という条件は最大5回のループで必ず偽になります。したがって、このプログラムは必ず停止し、全正当性も証明されます。
x := 0;
while x < 5 do
x := x + 1;
end while;
| 実行ステップ | x の値 | 条件評価 | ループ不変式 | 停止? |
|---|---|---|---|---|
| 初期状態 | 0 | 0 < 5 = true | 0 ≤ x ≤ 5 ✓ | No |
| ループ1回目 | 1 | 1 < 5 = true | 0 ≤ x ≤ 5 ✓ | No |
| ループ2回目 | 2 | 2 < 5 = true | 0 ≤ x ≤ 5 ✓ | No |
| ループ3回目 | 3 | 3 < 5 = true | 0 ≤ x ≤ 5 ✓ | No |
| ループ4回目 | 4 | 4 < 5 = true | 0 ≤ x ≤ 5 ✓ | No |
| ループ5回目 | 5 | 5 < 5 = false | 0 ≤ x ≤ 5 ✓ | Yes |
結論: プログラムは5回のループ後に停止し、x = 5 となる
この表が示すプログラムの正当性
部分正当性: 初期条件 x = 0 から開始し、終了時には x = 5 となっています。ループ不変式 0 ≤ x ≤ 5 はすべての段階で保持されており、プログラムは仕様通りの結果を出力しています。
全正当性: プログラムは5回のループ後に必ず停止します。各ループで x は1ずつ増加し、条件 x < 5 は最終的に偽となるためです。
問題2: 停止問題について、なぜすべてのプログラムに対して全正当性を証明することができないのか説明しなさい。
解答例
停止問題は決定不能問題であり、任意のプログラムが停止するかどうかを判定する汎用アルゴリズムは存在しないことがチューリングによって証明されています。この証明は、「停止するかどうかを判定するプログラム」自体に対して矛盾が生じることを示す反証法によるものです。もし全てのプログラムに対して全正当性を証明できるなら、それは停止問題を解決できることを意味しますが、これは不可能であることが証明されています。したがって、すべてのプログラムに対して全正当性を一般的に証明することはできません。
5. まとめ
プログラムの正当性理論は、プログラムがその仕様に従って正しく動作することを形式的に証明するための重要な理論です。部分正当性と全正当性という2つの主要な概念があり、前者はプログラムの途中までの正しさを示し、後者はプログラムが必ず停止することを保証します。しかし、停止問題により、すべてのプログラムに対して全正当性を証明することはできません。プログラムの正当性は、安全性が求められるシステムにおいて特に重要であり、その証明は信頼性の高いシステム開発に不可欠です。
実際の開発現場では、完全な形式証明は複雑で時間がかかるため、重要なコンポーネントや安全性が特に求められる部分に対して選択的に適用されることが多いです。また、型システムやデザインバイコントラクトなどの手法も、プログラムの正当性を部分的に保証するために広く使われています。