SPARKによる形式検証入門 ── Adaの契約から数学的証明へ
· 小村 豪 · Ada, SPARK, FormalVerification, GNATprove, DesignByContract, HighIntegrity, ProgrammingLanguage, 形式検証, 高信頼性
1. はじめに ── 「動かして確かめる」の先へ
ソフトウェアの品質を保証する方法として、最も一般的なのはテストです。
テスト: 選んだ入力に対して正しく動くことを確認する
しかし、テストには限界があります。入力の組み合わせは無限にあり、「すべての入力で正しい」ことはテストだけでは示せません。
ここで登場するのが形式検証(Formal Verification)です。
形式検証: すべての入力に対して性質が成り立つことを数学的に証明する
前回の記事「Ada言語の魅力」では、Ada の全体像を紹介し、SPARK についても簡単に触れました。
この記事では、SPARK を使った形式検証の実践に焦点を絞り、次のことを整理します。
SPARKとは何か。Adaとの関係はどうなっているのか
契約(Pre/Post)をどう書くか
GNATproveでどう証明するか
ループ不変条件をどう設計するか
データフロー契約(Global/Depends)で副作用を管理する方法
証明レベル(Stone〜Platinum)の段階的な適用戦略
実プロジェクトへの組み込み方
テストから証明へのステップアップを、実際のコード例とともに体験できることを目指します。
なお、この記事に登場するコード断片は、章ごとにファイルへ整理した参照用コード集として GitHub で公開しています。
ada-spark-formal-verification - komurasoft-blog-samples (GitHub)
2. SPARKとは何か ── Adaの部分言語にして証明の世界への入り口
SPARK は、Ada のサブセット(部分言語)です。
サブセットであることには、明確な意図があります。
Adaの全機能 → 表現力は高いが、すべてを形式検証するのは現実的でない
SPARK → 検証可能な機能だけに絞り、証明を現実的にする
SPARK が制限する主なものは次のとおりです。
ポインタ(アクセス型)による動的メモリ管理 → 所有権モデルで制御
例外ハンドラーの自由な使用 → 制限付きで許容
再帰的なデータ構造 → 証明が困難なため制限
タスクの自由な使用 → Ravenscarプロファイルで制限
「制限」と聞くと窮屈に感じるかもしれません。しかし、これらの制限は証明可能性と引き換えに得られたものです。
SPARK のツールセットは、AdaCore が提供する GNATprove が中心です。
GNATproveの動作:
1. SPARKで書かれたAdaコードを解析する
2. 契約(Pre/Post)や表明をWhy3中間言語に変換する
3. Z3, CVC4, Alt-Ergoなどの自動証明器で証明を試みる
4. 結果をソースコード上のメッセージとして報告する
重要なのは、SPARK は Ada の上に構築されていることです。
SPARKコード = Adaコード + 契約注釈
つまり、普段の Ada 開発の延長線上に SPARK があります。特別な構文を覚え直す必要はありません。
3. GNATproveのインストールと最初の証明
まずは、GNATprove を動かす環境を整えます。
Alire を使えば、次のコマンドで SPARK 対応のプロジェクトを作成できます。
alr init --bin spark_demo
cd spark_demo
GNATprove は GNAT コンパイラに同梱されているため、alr build でビルドできる環境であれば、そのまま gnatprove コマンドが使えます。
最初の証明対象として、絶対値を返す関数を書いてみます。
package Simple_Proof with SPARK_Mode is
function Abs_Value (X : Integer) return Integer
with Post => Abs_Value'Result >= 0;
end Simple_Proof;
package body Simple_Proof with SPARK_Mode is
function Abs_Value (X : Integer) return Integer is
begin
if X < 0 then
return -X;
else
return X;
end if;
end Abs_Value;
end Simple_Proof;
注目すべきポイントを整理します。
with SPARK_Mode をパッケージ仕様と本体の両方に付ける
Post条件で「結果は0以上」という性質を宣言する
'Result属性で関数の戻り値を参照する
このコードに対して GNATprove を実行します。
gnatprove -P spark_demo.gpr
結果は次のようになります。
SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved
postcondition proved のメッセージ。これが、すべての Integer の入力に対して、戻り値が 0 以上であることが証明されたことを意味します。
この体験が、SPARK の入り口です。
4. 契約による設計の基礎 ── PreとPostの書き方
SPARK の証明は、契約を書くことから始まります。
契約は Ada 2012 の言語機能ですが、SPARK ではそれが証明の入力になります。
procedure Transfer (From, To : in out Account; Amount : Positive)
with Pre => From.Balance >= Amount,
Post => From.Balance = From.Balance'Old - Amount
and then
To.Balance = To.Balance'Old + Amount;
Pre と Post の設計指針を整理します。
Pre(事前条件):
呼び出し側の責任
「この条件を満たして呼び出せば、Postを保証する」
十分に弱く(呼び出し側が満たせる範囲で)、かつ必要なだけ強く
Post(事後条件):
実装側の責任
「呼び出し後の世界の状態がこうなっている」
'Old属性で呼び出し前の値を参照できる
強すぎると実装が窮屈に、弱すぎると有用な性質が証明できない
よくある間違いと対策も押さえておきます。
間違い1: Preが強すぎる
Pre => X > 0 and X < 100 and X /= 50 and ...
→ 呼び出し側が常に満たせる条件か確認する
→ テストが通るからといってPreを絞りすぎない
間違い2: Postが弱すぎる
Post => True
→ 何も保証していない。証明の意味がない
間違い3: 副作用をPostに書き忘れる
Post => Result = X * 2 (グローバル変数の更新を見落としている)
→ Global/Depends契約で副作用を明示する(9章)
5. オーバーフロー証明 ── 数値計算の安全性を保証する
SPARK の証明で、実務的に最も恩恵が大きいものの一つがオーバーフロー防止です。
次のコードを見てください。
procedure Increment (X : in out Integer)
with SPARK_Mode,
Pre => X < Integer'Last,
Post => X = X'Old + 1;
Pre => X < Integer'Last がキーです。この契約があれば、GNATprove は加算がオーバーフローしないことを証明できます。
契約がない場合、GNATprove はオーバーフローの可能性を警告します。
medium: overflow check might fail
より複雑な計算でも同様です。
function Average (A, B : Integer) return Integer
with SPARK_Mode,
Pre => (if A >= 0 and B >= 0 then A <= Integer'Last - B
elsif A < 0 and B < 0 then A >= Integer'First - B),
Post => (if A <= B then A <= Average'Result and Average'Result <= B
else B <= Average'Result and Average'Result <= A);
Pre が複雑に見えますが、これは「A と B の和がオーバーフローしない」という条件を、符号を考慮して場合分けしたものです。
ポイント:
オーバーフロー証明の本質は、加算/乗算の前に「結果が型の範囲に収まる」
という条件をPreで宣言すること
面倒に見えるが、一度書けば二度とオーバーフローバグに悩まされない
6. ループ不変条件 ── ループの性質を証明する
形式検証で最も難しい部分の一つが、ループの証明です。
ループは任意の回数実行されるため、テストでは全パターンをカバーできません。SPARK ではループ不変条件(Loop Invariant)を使って証明します。
function Sum_Of_Naturals (N : Natural) return Natural
with SPARK_Mode,
Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;
function Sum_Of_Naturals (N : Natural) return Natural is
Result : Natural := 0;
begin
for I in 1 .. N loop
Result := Result + I;
pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
end loop;
return Result;
end Sum_Of_Naturals;
ループ不変条件の設計には、次の考え方が必要です。
1. ループの各反復の開始時点で成り立つ性質を書く
2. ループの最終反復後に、求めるPost条件が導けるものを選ぶ
3. 不変条件は、その時点までの計算結果を数式で表現する
もう一つ、配列探索の例を見てみます。
function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
with SPARK_Mode,
Post => (if Find'Result = 0 then
(for all K in Arr'Range => Arr (K) /= Target)
else
Arr (Find'Result) = Target);
function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
for I in Arr'Range loop
if Arr (I) = Target then
return I;
end if;
pragma Loop_Invariant
(for all K in Arr'First .. I => Arr (K) /= Target);
end loop;
return 0;
end Find;
ここでの不変条件は「ここまで調べた範囲には Target は存在しない」です。
ループ不変条件設計の原則:
「ループを n 回回った時点で、何が言えるか」を数式で表現する
配列ループでは「処理済み範囲について〜が成り立つ」の形が多い
不変条件が強すぎると証明できない。弱すぎるとPostが導けない
このバランスを取るのが、ループ証明の腕の見せ所
7. 表明プラグマ ── コード中に書く部分的な性質
契約(Pre/Post)に加えて、SPARK ではコードの途中に表明(Assert)を書けます。
procedure Divide (A, B : Integer; Q, R : out Integer)
with SPARK_Mode,
Pre => B /= 0,
Post => A = Q * B + R and R >= 0 and R < abs (B);
procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
Q := A / B;
R := A rem B;
pragma Assert (A = Q * B + R);
pragma Assert (R >= 0);
pragma Assert (R < abs (B));
end Divide;
プラグマの使い分けを整理します。
Pre/Post: サブプログラムの入口と出口での約束
Assert: コードの特定地点で成り立つべき性質
Loop_Invariant:ループの各反復で保たれる性質
Loop_Variant: ループが必ず終了することを示すための減少量
Assert の活用場面は次のようなものです。
複雑な計算の中間結果の確認
if/else分岐後の状態確認
手続き呼び出し後の戻り値の性質確認
後続の証明のための補題の提供
8. データフロー契約 ── GlobalとDepends
SPARK の強力な機能の一つが、データフロー契約です。
サブプログラムが読む/書くグローバル変数を明示します。
package Counter_Unit with SPARK_Mode is
Count : Natural := 0;
procedure Increment
with Global => (In_Out => Count);
procedure Reset
with Global => (Output => Count);
function Get_Value return Natural
with Global => (Input => Count);
end Counter_Unit;
Global 契約のモードは次の 3 つです。
Input: 読むだけ(関数向け)
Output: 書くだけ(初期化向け)
In_Out: 読み書きする(更新向け)
さらに、変数間の依存関係を Depends で表現できます。
procedure Transfer
(From, To : in out Account_Type)
with Global => (Input => Exchange_Rate),
Depends => (From =>+ (From, Exchange_Rate),
To =>+ (To, Exchange_Rate));
=>+ は「以前の値に加えて、これらの入力にも依存する」という意味です。
データフロー契約のメリット:
1. 「この関数は何に触るのか」が一目で分かる
2. 意図しない副作用をコンパイル時に検出できる
3. 変数の情報フロー解析の入力になる
4. 大規模システムでのデータの流れの可視化に役立つ
9. 証明レベル ── StoneからPlatinumへの段階的適用
SPARK には 証明レベル(Proof Level) という概念があります。
すべてのコードを一度に完全証明しようとすると、挫折しがちです。そこで SPARK は、段階的に証明の厳しさを上げていく戦略を提供しています。
Stone (レベル0):
契約の構文と型の整合性検査のみ
最初に到達すべきレベル
Bronze (レベル1):
Stone + 初期化されていない変数の読み取りがないことの証明
基本的な正当性の保証
Silver (レベル2):
Bronze + 実行時エラー(範囲外、オーバーフロー、ゼロ除算)が
起きないことの証明
最も実用的な目標
Gold (レベル3):
Silver + Pre/Post条件の証明
完全な機能正当性の保証
Platinum (レベル4):
Gold + データの非依存性・情報フローの証明
セキュリティ重視のシステム向け
実践的な導入戦略は次のようになります。
第1段階: プロジェクト全体をStoneレベルで通す
→ 契約の書き間違いを見つける
第2段階: 重要なモジュールをSilverレベルにする
→ オーバーフローや範囲外アクセスを撲滅する
→ 実務上のバグの多くはここで防げる
第3段階: 中核ロジックをGoldレベルにする
→ 機能正当性を数学的に保証する
→ アルゴリズムの正しさを証明する
第4段階: セキュリティ要件がある場合Platinumへ
→ 情報漏洩パスの検出
10. 実践的な証明の流れ ── 手戻りを減らすワークフロー
GNATprove を日常的に使うためのワークフローを紹介します。
1. 型と仕様を設計する
範囲制約、型不変条件を決める
2. 契約(Pre/Post)を書く
実装の前に仕様を契約として表現する
3. コンパイルを通す
GNATでコンパイルエラーを解消する
4. StoneレベルでGNATproveを実行する
gnatprove -P proj.gpr --level=0
5. 警告を確認し、必要に応じて契約を修正する
特に初期化漏れに注意
6. Silverレベルを目指す
gnatprove -P proj.gpr --level=2
実行時エラーを撲滅する
7. ループがあれば不変条件を追加する
証明できない場合、不変条件が不足していないか確認する
8. Goldレベルで機能正当性を証明する
gnatprove -P proj.gpr --level=3
よくある「証明できない」ケースとその対処法です。
ケース1: 「medium: postcondition might fail」
→ Post条件が強すぎるか、Pre条件が弱すぎる
→ あるいはループ不変条件が不足している
ケース2: 「medium: overflow check might fail」
→ Pre条件で値の範囲を制限する
→ または型自体の範囲を狭める
ケース3: 「medium: array index check might fail」
→ ループ範囲が配列範囲内であることを不変条件で示す
→ for I in Arr'Range を使用する(SPARKが範囲の自動認識を助ける)
ケース4: 「prover timeout」
→ 証明器が時間切れ。不変条件で段階的に分割する
→ 関数を小さく分割する
11. SPARKとテストの併用 ── 補完関係を理解する
形式検証とテストは、対立するものではなく補完し合います。
SPARKの証明:
すべての入力に対して性質が成り立つ
契約に書いた性質だけが対象
証明できないケースでは、手動確認やテストに委ねる
テスト:
選んだ入力に対して実際の動作を確認する
契約に書かれていない暗黙の前提も発見できる
実行環境との相互作用を確認できる
併用のパターンです。
1. SPARKでSilverレベル(実行時エラーなし)を保証
2. 単体テストで具体的な入出力の正しさを確認
3. Goldレベルでコアロジックを証明
4. 証明できない部分に集中的にテストを書く
Ada には AUnit という単体テストフレームワークがあります。SPARK で型と契約を固め、AUnit で振る舞いをテストする、という組み合わせが実践的です。
12. GNATproveの結果を読む ── メッセージの解釈
GNATprove の出力には、次の 3 つのレベルがあります。
info: 証明に成功した
medium: 証明できなかった(警告)。手動確認が必要
high: 証明に失敗した(エラー)。契約違反の可能性が高い
よくあるメッセージとその意味です。
「postcondition proved」 Post条件が証明された
「range check proved」 範囲チェックが証明された
「overflow check proved」 オーバーフローしないことが証明された
「index check proved」 配列添字の範囲が証明された
「divide by zero check proved」 ゼロ除算が起きないことが証明された
「might fail」 証明できなかった
「cannot prove」 証明器が証明を完了できなかった
「prover timeout」 制限時間内に証明が完了しなかった
might fail が出たときの対応手順です。
1. 本当に失敗しうるのか、コードを読んで判断する
2. 失敗しうるなら、コードを修正する
3. 失敗しないはずなら、契約(Pre/不変条件)を強化する
4. それでも証明できないなら、pragma Assume で仮定として宣言する
(ただし、Assumeは未証明の仮定なので注意)
13. 実プロジェクトへの組み込み方
既存のプロジェクトに SPARK を導入する際の現実的なアプローチです。
1. 新規コードから始める
既存コード全体を一度にSPARK化しようとしない
新しく書くモジュールからSPARK_Modeを有効にする
2. Silverを目標にする
Gold(完全機能証明)は理想的だが、Silver(実行時エラーなし)から始める
オーバーフロー防止だけでも、実務上の価値は非常に大きい
3. インターフェースから契約を書く
実装より先に、パッケージ仕様(.ads)に契約を書く
仕様が固まっていれば、実装者が誰でも契約を満たすコードを書ける
4. CI/CDに組み込む
gnatproveをCIパイプラインに追加する
証明に失敗したらビルドを止める(または警告を出す)
5. 証明レポートを蓄積する
gnatprove --report=all でレポートを生成する
未証明項目の推移を追う
C/C++ の既存コードが混在するプロジェクトでは、次の段階的アプローチが有効です。
1. 新規モジュールはAda/SPARKで書く
2. C/C++とはInterfaces.C経由で連携する
3. 重要なデータ構造と検証ロジックをSPARKに移行する
4. 段階的にSPARKの範囲を広げる
14. SPARKの限界と注意点
SPARK も万能ではありません。限界を正直に理解しておくことが、正しい適用につながります。
証明できる範囲:
SPARKが証明するのは「契約に書いた性質」だけ
契約の漏れ(書き忘れた性質)は証明されない
例: Postでソート済みを証明しても、「破壊的でないこと」を書き忘れると
元の要素が保存されることは保証されない
証明器の限界:
自動証明器では証明できない複雑な性質がある
その場合は手動証明(Coqなど)に頼る必要がある
とはいえ、実務の範囲では自動証明で十分なことが多い
言語の制限:
ポインタを多用するコードはSPARK化できない
動的メモリ確保の証明は限定的
再帰的データ構造の証明は難しい
開発者の習熟:
契約の書き方には訓練が必要
ループ不変条件の設計は特に習得に時間がかかる
チーム全体のスキルアップ計画が不可欠
15. まとめ ── 証明を日常の開発に
SPARK による形式検証の実践を整理してきました。
SPARKはAdaのサブセットで、証明可能な機能に絞っている
契約(Pre/Post)が証明の入力になる。Ada 2012の契約をそのまま使える
GNATproveが自動証明を実行し、結果をソースコードレベルで報告する
ループ不変条件でループの性質を証明する
Global/Dependsでデータフローを明示し、副作用を管理する
証明レベル(Stone〜Platinum)で段階的に厳しさを上げていける
まずはSilverレベル(実行時エラーなし)を目指すのが実践的
テストと証明は対立するものではなく、補完し合う
「形式検証は難しくて、特別なプロジェクトだけのもの」という先入観があるかもしれません。
しかし、今日の SPARK と GNATprove の組み合わせは、次のレベルに到達しています。
1. 契約を書く。これは型やテストを書くのと本質的に同じ設計作業
2. gnatproveを実行する。コンパイルと同様の感覚
3. 結果を見て、コードか契約を修正する
このサイクルは、コンパイラのエラーメッセージを見ながらコードを修正する日常の開発フローと、何も変わりません。
違いは、コンパイラが「構文が正しい」を保証するのに対し、GNATprove が「すべての入力で正しい」を保証することです。
前回の記事で紹介した Ada のキャッチフレーズ「バグは見つけるものではなく、型と契約で書けなくするもの」は、SPARK によって次の段階に進みます。
バグの不在は、証明によって保証するもの。
まずは、小さな関数に SPARK_Mode と Post を付けて、gnatprove を実行してみてください。
postcondition proved の緑色のメッセージを見たとき、ソフトウェアの品質保証に対する見方が変わるはずです。
参考
- この記事のコード断片を章ごとに整理した参照用コード集 - komurasoft-blog-samples (GitHub)
- SPARK - AdaCore
- Introduction to SPARK - learn.adacore.com
- SPARK 2014 Reference Manual
- GNATprove User’s Guide
- Ada Reference Manual (Ada 2022)
- Alire - Ada Library Repository
- Why3 - Platform for Deductive Program Verification
- Ada言語の魅力 ── 型で設計を語り、数十年動き続けるソフトウェアを支える言語 - 当サイト
関連する記事
同じタグを共有する最新の記事です。さらに近い話題で知識を深められます。
Ada言語の魅力 ── 型で設計を語り、数十年動き続けるソフトウェアを支える言語
Ada言語の魅力を紹介します。強い型付け、範囲制約、パッケージによる仕様と実装の分離、契約による設計、言語組み込みのタスク、SPARKによる形式検証、GNATとAlireでの開発環境まで、高信頼ソフトウェアを支える設計思想を整理します。
Adaのジェネリックプログラミング ── 型で契約を書き、再利用をゼロコストで実現する
Adaのジェネリックプログラミングを、総称サブプログラム、総称パッケージ、仮サブプログラム、型カテゴリ、正式パッケージパラメータ、実務上の設計指針まで体系的に解説します。Mermaid図と実例を交え、型安全な再利用とゼロコスト抽象化の考え方を整理します。
Adaによるリアルタイムシステムプログラミング ── 優先度・周期・実行時間制御の実践
Ada の Annex D（リアルタイムシステム）が提供するリアルタイム機能——タスク優先度、Ceiling_Locking プロトコル、delay until による周期実行、Ravenscar プロファイル、タイミングイベント、保護キュー、タスク別実行時間計測、マルチ周...
Adaにおける安全な並行処理 ── タスクと保護オブジェクトの実践ガイド
Adaの言語組み込み並行処理であるタスクと保護オブジェクトの実践的な入門記事です。ランデブー(entry/accept)、選択的アクセプト、プロデューサー・コンシューマー、保護オブジェクトによる排他制御、バリア付き保護エントリ、タイムアウト付き呼び出し、タスク優先度とリアル...
Fableが使えなくなったけど諦めるな ── OpenRouter Fusion＋中華LLM＋レビュー層で凌ぐ
Fableには遠く及びません。ですがOpenRouter Fusionで5つの中華LLMを組み合わせ、gpt-5.5-pro または Codex PRレビューを重ねれば、素のgpt-5.5よりはずっとマシなコーディングエージェントになります。
関連トピック
このテーマと近いトピックページです。記事を起点に、関連するサービスや他の記事へ進めます。
Windows技術トピック
Windows 開発、不具合調査、既存資産活用の技術トピックをまとめた入口です。
著者プロフィール
記事の著者プロフィールページです。
小村 豪
合同会社小村ソフト 代表
Windows ソフト開発、技術相談、不具合調査を中心に、既存資産が残る案件や原因が見えにくい障害調査に強みがあります。
公開リンク