SPARKによる形式検証入門 ── Adaの契約から数学的証明へ

1. はじめに ── 「動かして確かめる」の先へ

ソフトウェアの品質を保証する方法として、最も一般的なのはテストです。

テスト: 選んだ入力に対して正しく動くことを確認する

しかし、テストには限界があります。入力の組み合わせは無限にあり、「すべての入力で正しい」ことはテストだけでは示せません。

ここで登場するのが形式検証(Formal Verification)です。

形式検証: すべての入力に対して性質が成り立つことを数学的に証明する

前回の記事「Ada言語の魅力」では、Ada の全体像を紹介し、SPARK についても簡単に触れました。

この記事では、SPARK を使った形式検証の実践に焦点を絞り、次のことを整理します。

SPARKとは何か。Adaとの関係はどうなっているのか
契約(Pre/Post)をどう書くか
GNATproveでどう証明するか
ループ不変条件をどう設計するか
データフロー契約(Global/Depends)で副作用を管理する方法
証明レベル(Stone〜Platinum)の段階的な適用戦略
実プロジェクトへの組み込み方

テストから証明へのステップアップを、実際のコード例とともに体験できることを目指します。

この記事の対象読者と前提知識

想定している読者は次のような方です。

• Ada の基本的な文法（パッケージ、in / out / in out のパラメータモード、型と部分型）を一度は見たことがある方
• 契約プログラミングや静的解析に関心があり、「テストの次」を探している方
• 高信頼性・組込み・制御系のソフトウェアで、品質保証の手段を検討している方

Ada 未経験でも読めますが、前提を 2 つだけ補っておきます。 本記事のコード例には、package ... is と package body ... is によるパッケージの仕様部と本体の分離、そして procedure P (X : in out Integer) のようなパラメータモードが繰り返し出てきます。この 2 つに見覚えがない場合は、先に「Ada言語の魅力」で Ada 側の基礎を押さえてから戻ってくると、契約の話に集中できます。

逆に言えば、この 2 つさえ分かれば読み進められます。SPARK 固有の記法（SPARK_Mode、Pre、Post、Loop_Invariant、Global、Depends）は、すべてこの記事の中で説明します。証明器の理論や論理学の知識も必要ありません。GNATprove が出したメッセージを読んで、コードか契約を直す。実際に必要なのはそれだけです。

なお、この記事に登場するコード断片は、章ごとにファイルへ整理した参照用コード集として GitHub で公開しています。

ada-spark-formal-verification - komurasoft-blog-samples (GitHub)

この記事の知識マップ

SPARKはAdaの契約機能を土台にした証明可能なサブセット言語で、Pre/Post契約やループ不変条件、副作用を明示するGlobal/Depends契約を証明の入力として、GNATproveがWhy3中間言語経由でZ3やcvc5などのSMTソルバに証明を委ねる。証明の厳しさはStoneからPlatinumまで5段階の証明レベルで定義され、実行時エラーの不在を保証するSilverレベルが実務での既定の到達目標とされる。タスクを扱う場合はRavenscarプロファイルへの制限が前提となり、GNAT環境の構築にはAlireが使われる。形式検証は選んだ入力だけを確認するテストと対立せず、AUnitによる単体テストと組み合わせて証明できない部分を補うことが実践的な運用として推奨される。

flowchart LR
    accTitle: SPARKによる形式検証の知識マップ
    accDescr: SPARKがAdaの契約機能を土台にGNATproveとWhy3・SMTソルバで証明を行うこと、ループ不変条件やデータフロー契約が証明の入力になること、証明レベルがStoneからPlatinumまで段階的に定義されSilverが実務上の目標とされること、テストとの補完関係を示す図。
    spark["SPARK"]
    formal_verification["形式検証"]
    ada["Ada(プログラミング言語)"]
    design_by_contract["契約による設計(Pre/Post)"]
    gnatprove["GNATprove"]
    why3["Why3"]
    smt_solver["SMTソルバ(自動証明器)"]
    loop_invariant["ループ不変条件(Loop Invariant)"]
    dataflow_contract["データフロー契約(Global/Depends)"]
    spark_proof_level["証明レベル(Stone〜Platinum)"]
    ravenscar_profile["Ravenscarプロファイル"]
    alire["Alire"]
    aunit["AUnit"]
    spark_silver_level["Silverレベル(AoRTE)"]
    spark -->|"利用する"| ada
    spark -->|"実装を担う"| formal_verification
    spark -.->|"前提とする"| design_by_contract
    spark -->|"利用する"| gnatprove
    gnatprove -->|"前提とする"| ada
    gnatprove -->|"利用する"| why3
    why3 -->|"利用する"| smt_solver
    spark -.->|"前提とする"| loop_invariant
    spark -->|"利用する"| dataflow_contract
    spark -->|"利用する"| spark_proof_level
    spark -.->|"前提とする"| ravenscar_profile
    ada -.->|"で構成できる"| alire
    aunit -->|"推奨される対応"| spark
    spark_silver_level -->|"推奨される対応"| spark
    spark_silver_level -->|"で確認できる"| gnatprove
    dataflow_contract -->|"で確認できる"| gnatprove
    design_by_contract -->|"で確認できる"| gnatprove

図の実線は常に成り立つ関係、破線は条件付きの関係です(成立条件は詳細ページの各関係の説明に記載)。関係すべての一覧(全17件、根拠・確度つき)と主要概念の定義は知識マップ詳細ページにまとめています。データ: JSON-LD / Turtle

2. SPARKとは何か ── Adaの部分言語にして証明の世界への入り口

SPARK は、Ada のサブセット(部分言語)です。

サブセットであることには、明確な意図があります。

Adaの全機能 → 表現力は高いが、すべてを形式検証するのは現実的でない
SPARK       → 検証可能な機能だけに絞り、証明を現実的にする

SPARK が制限する主なものは次のとおりです。

ポインタ(アクセス型)による動的メモリ管理 → 所有権モデルで制御
例外ハンドラーの自由な使用               → 制限付きで許容
再帰的なデータ構造                       → 証明が困難なため制限
タスクの自由な使用                       → Ravenscarプロファイルで制限

「制限」と聞くと窮屈に感じるかもしれません。しかし、これらの制限は証明可能性と引き換えに得られたものです。

SPARK のツールセットは、AdaCore が提供する GNATprove が中心です。

GNATproveの動作:
1. SPARKで書かれたAdaコードを解析する
2. 契約(Pre/Post)や表明をWhy3中間言語に変換する
3. Z3、cvc5、Alt-Ergoなどの自動証明器で証明を試みる
4. 結果をソースコード上のメッセージとして報告する

図にすると、次のような流れです。

flowchart LR
    Src["SPARKで書かれたAdaコード<br/>Pre / Post / Assert"] --> GP[GNATprove]
    GP --> VC[検証条件の生成]
    VC --> Why3["Why3<br/>中間言語と証明プラットフォーム"]
    Why3 --> P1[cvc5]
    Why3 --> P2[Z3]
    Why3 --> P3[Alt-Ergo]
    P1 --> Res[結果の集約]
    P2 --> Res
    P3 --> Res
    Res --> Msg["ソースコード上の位置つきメッセージ<br/>info / medium / high"]

開発者が直接触るのは両端、つまり左のコードと右のメッセージだけです。中央の Why3 と証明器は自動で動くため、通常は意識する必要がありません。意識するのは、証明が通らずに証明器を切り替えたり時間をかけたりする段階になってからです。

この章で出てきた名前

初出の固有名詞をここで押さえておきます。以降は説明なしで使います。

重要なのは、SPARK は Ada の上に構築されていることです。

SPARKコード = Adaコード + 契約注釈

つまり、普段の Ada 開発の延長線上に SPARK があります。特別な構文を覚え直す必要はありません。

3. GNATproveのインストールと最初の証明

まずは、GNATprove を動かす環境を整えます。

Alire を入れる

GNATprove は GNAT ツールチェーンに同梱されています。そのツールチェーンを入手する最も手軽な方法が Alire です。Ada / SPARK 向けのソースベースのパッケージマネージャで、コマンド名は alr です。配布物は Alire の GitHub リポジトリのリリースページから入手します。

導入できたら、既定のコンパイラを選びます。

alr toolchain --select

選択アシスタントが起動し、導入可能な GNAT の一覧から既定のコンパイラを選べます。引数なしの alr toolchain を実行すると、導入済みのコンパイラと現在の既定が表示されます。

バージョンを確認する

環境ができたら、バージョンを控えておいてください。証明結果は証明器のバージョンに依存します。 あとで「同じコードが証明できなくなった」となったときに、最初に確認すべき情報です。

alr version
gnatprove --version

プロジェクトを作る

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 の入り口です。

証明できなかったときの出力

成功したときの出力だけを見ていても、実務で必要になるのは失敗したときの読み方です。GNATprove は、証明できなかったチェックをソースコード上の位置つきで報告します。基本の形は次の 1 行です。

file.adb:12:37: medium: divide by zero might fail

file.adb の 12 行 37 列、つまり除算記号 / のある位置について、「除数が 0 でないことを証明できなかった」という意味です。ここで大事なのは、might fail（失敗するかもしれない）であって will fail（失敗する）ではないことです。本当にバグがあるとは限りません。 情報が足りず証明器が判断できなかっただけ、というケースが大半です。

反例が得られた場合は、より詳しい形で報告されます。

high: assertion might fail
--> counterex.adb:11:25
 11 |    pragma Assert (R < 42);
    |                  ^~~~~~
  + e.g. when R = 42
  + provers gave up before completing the proof

e.g. when R = 42 が反例で、「R が 42 のときに成り立たない」と具体的に教えてくれます。契約の不足が原因だと GNATprove が推測した場合には、修正案が添えられることもあります。

possible fix: subprogram at line xxx should mention Var in a precondition
possible fix: loop at line xxx should mention Var in a loop invariant
possible fix: call at line xxx should mention Var in a postcondition

この種のメッセージは、自分で意図的に出してみるのが一番早く慣れます。たとえば上の Abs_Value の Post を Abs_Value'Result > 0（0 より大きい）に変えると、X = 0 のケースを証明できずに postcondition might fail が出ます。5 章で扱う Increment から Pre を外せば overflow check might fail が出ます。成功例と失敗例を交互に出しながら進めるのが、GNATprove に慣れる近道です。

なお、メッセージの重大度（info / medium / high）とチェック種別の一覧は 12 章で整理します。

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契約で副作用を明示する(8章)

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)
  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:
  SPARKのサブセットとして妥当なコードであることの確認
  導入の途中段階として使う

Bronze:
  Stone + 初期化されていない変数を読まないこと、
  データフローが意図通りであることの保証
  できるだけ広い範囲に適用する

Silver:
  Bronze + 実行時エラー(範囲外、オーバーフロー、ゼロ除算)が
  起きないことの証明 (AoRTE: Absence of Run-time Errors)
  クリティカルなソフトウェアの既定の目標

Gold:
  Silver + 重要な integrity プロパティ
  (安全性・セキュリティ上の鍵となる性質)の証明
  そうした性質を持つ一部のコードに限って適用する

Platinum:
  要求仕様の完全な機能正当性の証明
  最高水準の要求がある部分にのみ適用する
  コストが高く、適用例は多くない

「レベル」という言葉が指すもの ── --mode と --level は別物

ここで混同しやすい点を整理しておきます。Stone〜Platinum はソフトウェア保証のレベルであり、gnatprove の --level オプションとは別の概念です。前者に対応するのは --mode のほうです。

Silver、Gold、Platinum は同じスイッチで起動します。違いはツールの動かし方ではなく、何をどこまで検証対象と定めるかという目標設定の側にあります。

一方 --level=0 〜 --level=4 は、証明にどれだけ手間をかけるかを決めるプリセットです。値を上げるほど時間はかかりますが、証明力は上がります。中身は個別スイッチの組み合わせで、次のようになっています。

つまり --mode が「何を検証するか」、--level が「どれだけ粘るか」です。まず意識すべきは --mode のほうで、--level は証明が通らないときに上げていく調整つまみだと考えてください。

もう 1 点、実務上の注意があります。--level は制限時間で制御するため、マシンの性能や負荷によって結果が変わり、再現性がありません。 CI や複数人で結果を共有する場面では、時間ではなく推論ステップ数で上限を決める --steps か、既存の証明結果を再生する --replay を使うことが公式に推奨されています。

出典: SPARK User’s Guide（8.1 Levels of Software Assurance、および Appendix A Command Line Invocation）

実践的な導入戦略は次のようになります。

第1段階: プロジェクト全体をStoneレベルで通す
  → 契約の書き間違いを見つける

第2段階: 重要なモジュールをSilverレベルにする
  → オーバーフローや範囲外アクセスを撲滅する
  → 実務上のバグの多くはここで防げる

第3段階: 中核ロジックをGoldレベルにする
  → 安全性・セキュリティの鍵となる性質を数学的に保証する
  → コード全体ではなく、その性質を持つ部分に絞る

第4段階: 最高水準の要求がある部分だけPlatinumへ
  → 要求仕様の完全な機能正当性を証明する
  → コストが高いため、適用範囲は最小限にする

10. 実践的な証明の流れ ── 手戻りを減らすワークフロー

GNATprove を日常的に使うためのワークフローを紹介します。

1. 型と仕様を設計する
   範囲制約、型不変条件を決める

2. 契約(Pre/Post)を書く
   実装の前に仕様を契約として表現する

3. コンパイルを通す
   GNATでコンパイルエラーを解消する

4. StoneレベルでGNATproveを実行する
   gnatprove -P proj.gpr --mode=stone

5. 警告を確認し、必要に応じて契約を修正する
   特に初期化漏れに注意
   初期化とデータフローだけを見るならBronze
   gnatprove -P proj.gpr --mode=bronze

6. Silverレベルを目指す
   gnatprove -P proj.gpr --mode=silver
   実行時エラーを撲滅する

7. ループがあれば不変条件を追加する
   証明できない場合、不変条件が不足していないか確認する

8. Goldレベルで重要な性質を証明する
   gnatprove -P proj.gpr --mode=gold
   起動スイッチはSilverと同じで、変わるのは検証の目標のほう
   時間内に証明が終わらないときだけ --level を上げて粘る
   例: gnatprove -P proj.gpr --mode=gold --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(重要な完全性の証明)やPlatinum(完全機能証明)は理想的だが、
   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言語の魅力 ── 型で設計を語り、数十年動き続けるソフトウェアを支える言語 - 当サイト

関連する記事

同じタグを共有する最新の記事です。さらに近い話題で知識を深められます。

関連トピック

このテーマと近いトピックページです。記事を起点に、関連するサービスや他の記事へ進めます。

よくある質問

この記事のテーマについて、相談時によくある質問をまとめています。

SPARKとは何ですか？Adaとはどんな関係ですか？

SPARKはAdaのサブセット（部分言語）で、プログラムの性質を数学的に証明できるように設計されています。ポインタによる動的メモリ管理や自由な例外使用などを制限する代わりに、証明可能性を得ています。SPARKコードはAdaコードに契約注釈を加えたものなので、普段のAda開発の延長線上にあり、特別な構文を覚え直す必要はありません。ツールはAdaCoreが提供するGNATproveが中心で、契約をWhy3中間言語に変換し、Z3などの自動証明器で証明を試みます。

形式検証はテストと何が違いますか？

テストは「選んだ入力に対して正しく動くこと」を確認するのに対し、形式検証は「すべての入力に対して性質が成り立つこと」を数学的に証明します。入力の組み合わせは無限にあるため、テストだけでは全入力での正しさは示せません。ただし両者は対立するものではなく補完関係にあり、SPARKでSilverレベル（実行時エラーなし）を保証し、単体テストで具体的な入出力を確認し、証明できない部分に集中的にテストを書く併用が実践的です。

SPARKの証明レベル（Stone〜Platinum）とは何ですか？

段階的に証明の厳しさを上げていくための概念です。Stoneは有効なSPARKであること、Bronzeは未初期化変数の読み取りがなくデータフローが正しいことの証明、Silverは実行時エラー（範囲外、オーバーフロー、ゼロ除算）が起きないことの証明です。Goldはそこに、重要なデータ不変条件が保たれることや状態遷移が仕様どおりであることといった、鍵となる完全性（integrity）の性質の証明を加えます。Platinumは契約が機能要件を網羅し、実装が仕様どおりであることを証明する完全な機能正当性のレベルで、コストが高く到達例は多くありません。実務ではまずSilverレベルを目指すのが最も実用的な目標とされています。

GNATproveで証明できないときはどうすればよいですか？

メッセージ別に対処します。「postcondition might fail」はPost条件が強すぎるかPre条件が弱すぎる、あるいはループ不変条件の不足が原因です。「overflow check might fail」はPre条件で値の範囲を制限するか型自体の範囲を狭めます。「array index check might fail」はループ範囲が配列範囲内であることを不変条件で示します。「prover timeout」は不変条件で証明を段階的に分割するか、関数を小さく分割します。本当に失敗しうるのかコードを読んで判断することが最初のステップです。

著者プロフィール

記事の著者プロフィールページです。

小村 豪

合同会社小村ソフト 代表

Windows ソフト開発、技術相談、不具合調査を中心に、既存資産が残る案件や原因が見えにくい障害調査に強みがあります。