AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる

AIに関数を書かせると、普通の値を入れたテストはたいてい通ります。困るのは、整数の上限近くの値や空の配列のように、テストに書かなかった入力で落ちるコードです。SPARKのGNATproveは事前条件を満たすすべての入力について、実行時エラーが起きないことと事後条件が成り立つことを確かめます。テストの入力を選ぶ必要はありません。

この記事ではAIに書かせたという想定の小さな関数を3つ使い、事前条件（Pre）と事後条件（Post）を付けてGNATproveにかけます。失敗したときのメッセージの読み方と直し方を実際の出力で示し、証明が保証することとしないことを分けます。最後に、AIのコードをレビューするとき人が何を読むかをまとめます。

SPARKとGNATproveの基本（インストール、証明レベル、データフロー契約など）は「SPARKによる形式検証入門」で説明しています。この記事では繰り返しません。

例はすべて Linux（x86_64）で実行しました。証明には GNAT FSF ビルドの gnatprove 15.1.0-1（--version の表示は FSF 15.0、同梱の証明器は Alt-Ergo 2.6.0・cvc5 1.2.1・Z3 4.13.4）を使い、実行には GNAT 13.3.0 を使っています。コマンドは特に断らない限り gnatprove -P p.gpr --level=2 --report=fail です。

人が書く契約とAIが書く本体

この記事で扱う進め方では、関数の仕様部（.ads）にある契約を人が書き、本体（.adb）をAIに書かせます。GNATproveの結果が失敗なら、メッセージをAIに渡して本体を直させます。証明が通ったら、人は本体よりも契約を読み直します。

flowchart TB
        accTitle: 契約と本体の分担
        accDescr: 人が事前条件と事後条件を書き、AIが本体を書き、GNATproveで証明し、失敗したらメッセージを渡して直させ、通ったら人が契約を読み直す流れを示す。
        A["人がPreとPostを書く"] --> B["AIが本体を書く"]
        B --> C["GNATproveで証明する"]
        C -->|"失敗"| D["メッセージをAIに渡す"]
        D --> B
        C -->|"すべて証明済み"| E["人が契約を読み直す"]

図1: 人が契約を書き、AIが本体を書き、GNATproveの結果で直させる流れ。

この分担にするのは、証明が「本体が契約を満たすこと」しか確かめないからです。契約が仕様を正しく表しているかは、人が判断するしかありません。後の節で、弱い契約のまま証明が通る例を見ます。AdaCoreの資料も仕様部（低レベルの要求）を定義する人と、対応する本体を書く人を分ける進め方を挙げています¹。

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

例1: 2つの整数の平均

最初の例は2つの Integer の平均を返す関数です。事後条件で、結果が2つの値の間に入ることを求めます。

package Averages with SPARK_Mode is

   function Average (A, B : Integer) return Integer
     with Post => Average'Result in Integer'Min (A, B) .. Integer'Max (A, B);

end Averages;

足し算のあふれ

AIが最初に書いた本体は次の式だとします。

package body Averages with SPARK_Mode is

   function Average (A, B : Integer) return Integer is
   begin
      return (A + B) / 2;
   end Average;

end Averages;

GNATproveの出力は次のとおりです。

averages.adb:5:17: high: overflow check might fail, cannot prove lower bound for (A + B)
    5 |      return (A + B) / 2;
      |             ~~~^~~~
  e.g. when A = Integer'First
        and B = -1
  reason for check: result of addition must fit in a 32-bits machine integer
  possible fix: add precondition (if B >= 0 then A <= Integer'Last - B else A >= Integer'First - B) to subprogram at averages.ads:3
    3 |   function Average (A, B : Integer) return Integer
      |            ^ here

1行目はファイル・行・列、重大度（high）、検査の種類（overflow check）、証明できなかった理由です。e.g. when の行は反例で、A = Integer'First、B = -1 のとき A + B が Integer の範囲を下に外れることを示します。possible fix は証明を通すための事前条件の案です。

flowchart TB
        accTitle: GNATproveの失敗メッセージの読み方
        accDescr: 失敗メッセージの1行目が場所と重大度と検査の種類を示し、反例の行が誤る入力の例を、理由の行が検査の中身を、提案の行が証明を通す事前条件の案を示すことを表す。
        A["1行目: 場所・重大度・検査の種類"] --> B["e.g. when: 反例の値"]
        B --> C["reason for check: 検査の中身"]
        C --> D["possible fix: 事前条件の案"]
        B -.-> E["反例の値で実行して確かめる"]

図2: 失敗メッセージは場所、反例、理由、提案の順に並ぶ。

反例が本当に誤りを示しているかは、その値で実行すると確かめられます。GNAT 13.3.0 でアサーションを有効にする -gnata を付けてビルドし、(2, 8)、(-7, 3)、(Integer'Last, Integer'Last)、(Integer'First, -1) の順に呼びました。

 5
-2

raised CONSTRAINT_ERROR : averages.adb:5 overflow check failed

普通の値の2つは正しく、3つ目の呼び出しで Constraint_Error になりました。Adaでは、値が型の基本範囲に収まるかを確かめる Overflow_Check に失敗すると、この例外が送出されます²。普通の値だけを入れたテストなら、この本体は通ります。

AdaCoreの資料によると、反例は実行できる入力に必ず対応するとは限りません。反例を調べた結果で、メッセージの重大度が medium から high に上がることもあります³。同じ本体を --level=1 で証明したときは、重大度が medium で、e.g. の行は出ませんでした。

引き算に移したあふれ

次に、あふれを避けるつもりで、AIが A + (B - A) / 2 に書き直したとします。この形では A <= B が前提になるので、事前条件も付けています。

   function Average (A, B : Integer) return Integer
     with Pre  => A <= B,
          Post => Average'Result in A .. B;

本体は return A + (B - A) / 2; です。結果は次のとおりで、今度は引き算があふれます。

averages.adb:5:21: high: overflow check might fail, cannot prove upper bound for (B - A)
    5 |      return A + (B - A) / 2;
      |                 ~~~^~~~
  e.g. when A = Integer'First
        and B = 0
  reason for check: result of subtraction must fit in a 32-bits machine integer

A <= B でも、A が Integer'First で B が0以上なら、B - A は Integer'Last を超えます。足し算を引き算に変えただけで、あふれる入力が別の範囲に移っています。

符号で場合を分ける

符号が同じなら引き算、違うなら足し算を使うと、どちらもあふれません。事前条件は最初の本体と同じく付けません。

package body Averages with SPARK_Mode is

   function Average (A, B : Integer) return Integer is
   begin
      if (A >= 0) = (B >= 0) then
         --  同じ符号なので、B - A は Integer に収まる
         return A + (B - A) / 2;
      else
         --  符号が異なるので、A + B は Integer に収まる
         return (A + B) / 2;
      end if;
   end Average;

end Averages;

この本体では --report=fail の出力が空になりました。--report=all にすると、証明できた検査も1行ずつ表示されます。

Long_Long_Integer（この環境のGNATでは64ビット）で足してから2で割る本体も、同じく全部証明できました。

   function Average (A, B : Integer) return Integer is
      Sum : constant Long_Long_Integer :=
        Long_Long_Integer (A) + Long_Long_Integer (B);
   begin
      return Integer (Sum / 2);
   end Average;

flowchart TB
        accTitle: 平均の関数の3つの本体
        accDescr: A足すBを2で割る本体は足し算があふれ、AにBとAの差の半分を足す本体は引き算があふれ、符号で場合を分ける本体はすべて証明できたことを示す。
        A["（A + B）/ 2"] --> R1["足し算があふれる"]
        B["A + （B - A）/ 2"] --> R2["引き算があふれる"]
        C["符号で場合を分ける"] --> R3["すべて証明済み"]
        R1 -.-> N1["反例 A = Integer'First, B = -1"]
        R2 -.-> N2["反例 A = Integer'First, B = 0"]

図3: 平均の関数の3つの本体と、GNATproveの結果。

提案された事前条件を足した場合

possible fix の事前条件を最初の本体にそのまま足すと、証明は通ります。ただし、関数が受け付ける入力が狭まります。Average (Integer'First, -1) は契約違反になり、呼び出し側がそうした値を渡さないことを示す必要が出ます。

証明を通すだけなら、AIは本体を直す代わりに事前条件を足すかもしれません。それが仕様として許されるかは、関数がどんな値を受け取るかで決まり、証明ツールには判断できません。

flowchart TB
        accTitle: 失敗したときの2つの直し方
        accDescr: 証明が失敗したとき、事前条件を足すと受け付ける入力が狭まり呼び出し側に条件が移り、本体を直すとすべての入力を受け付けたまま証明できることを示す。
        A["あふれの検査が失敗"] --> B["事前条件を足す"]
        A --> C["本体を直す"]
        B --> D["受け付ける入力が狭まる"]
        D --> E["呼び出し側が条件を守る"]
        C --> F["すべての入力を受け付ける"]

図4: 事前条件を足すと、条件を守る責任が呼び出し側に移る。

例2: 値を範囲に収める Clamp

2つ目の例は X を Lo 以上 Hi 以下に収める関数です。AIに契約まで書かせて、次の事後条件が返ってきたとします。

package Clamps with SPARK_Mode is

   function Clamp (X, Lo, Hi : Integer) return Integer
     with Pre  => Lo <= Hi,
          Post => Clamp'Result in Lo .. Hi;

end Clamps;

本体が return Integer'Max (Lo, Integer'Min (X, Hi)); なら、証明はすべて通ります。

弱い事後条件のまま通る誤り

この事後条件は結果が範囲に入ることしか求めていません。本体を return Lo; に変えても、証明はすべて通りました（X と Hi を使わない警告を消すため、pragma Unreferenced (X, Hi); を書いています）。

この本体を Clamp (5, 0, 10)、Clamp (-3, 0, 10)、Clamp (42, 0, 10) で実行した結果は、どれも0でした。具体的な期待値を書いたテストなら、すぐに失敗します。

事後条件を結果が1つに決まる形に書き直します。

   function Clamp (X, Lo, Hi : Integer) return Integer
     with Pre  => Lo <= Hi,
          Post => Clamp'Result =
                    (if X < Lo then Lo
                     elsif X > Hi then Hi
                     else X);

この契約では return Lo; の本体が証明できず、反例が出ます。

clamps.ads:5:19: high: postcondition might fail
    5>|          Post => Clamp'Result =
  ... | ...
    8 |                     else X);
  e.g. when Clamp'Result = 0
        and Hi = 1
        and Lo = 0
        and X = 1

Integer'Max と Integer'Min を使う本体は、この契約でもすべて証明できました。実行結果は 5、0、10 です。

flowchart TB
        accTitle: 事後条件の強さと証明の結果
        accDescr: 結果が範囲に入ることだけを求める事後条件では常にLoを返す本体も証明でき、結果を1つに決める事後条件ではその本体の証明が失敗することを示す。
        A["本体: 常に Lo を返す"] --> B["Post: 結果が Lo..Hi に入る"]
        A --> C["Post: 結果を1つに決める"]
        B --> D["証明が通る"]
        C --> E["事後条件の証明が失敗"]

図5: 同じ誤った本体でも、事後条件の強さで結果が変わる。

平均の例にも同じことが言えます。符号で分ける本体と64ビットで足す本体は、どちらも証明できました。それでも、Average (Integer'First, -1) の結果は前者が -1073741825、後者が -1073741824 で、一致しません。事後条件が「2つの値の間」としか言っていないので、どちらに丸めても契約を満たすからです。どちらに丸めるべきかは仕様の問題で、決めるのは人です。

事前条件がないとき

最初の事後条件のまま Pre => Lo <= Hi を消すと、正しい本体でも事後条件が証明できなくなります。反例は Lo = 1、Hi = 0 で、範囲が空なので、どの値を返しても Lo .. Hi に入りません。

SPARKの解析対象でないコードからこの関数を呼ぶ場合、呼び出し側が事前条件を守ることは、証明の前提として扱われます⁴。GNATでは -gnata を付けると事前条件と事後条件を実行時にも検査し、付けなければ検査しません⁵。実際に Clamp (5, 10, 0) を呼ぶと、-gnata 付きでは failed precondition from clamps.ads:4 の Assertion_Error になり、付けないと 10 を返しました。

例3: 配列の探索とループ不変条件

3つ目の例は配列から Key を探して位置を返し、見つからなければ0を返す関数です。

package Search with SPARK_Mode is

   type Int_Array is array (Positive range <>) of Integer;

   --  Key の位置を返す。見つからなければ 0 を返す。
   function Find (A : Int_Array; Key : Integer) return Natural
     with Post =>
       (if Find'Result = 0 then
          (for all I in A'Range => A (I) /= Key)
        else
          Find'Result in A'Range and then A (Find'Result) = Key);

end Search;

AIが書いた本体は for ループで先頭から比べるものです。

package body Search with SPARK_Mode is

   function Find (A : Int_Array; Key : Integer) return Natural is
   begin
      for I in A'Range loop
         if A (I) = Key then
            return I;
         end if;
      end loop;
      return 0;
   end Find;

end Search;

不変条件のない for ループ

この本体は正しいのに、見つからなかった場合の事後条件が証明できません。

search.ads:9:36: medium: postcondition might fail, cannot prove A (I) /= Key
    9 |          (for all I in A'Range => A (I) /= Key)
      |                                   ^~~~~~~~~~~~

今回は反例が付いていません。証明器はループが終わった時点で何が成り立つかを知らないので、「どの要素も Key ではない」と言えないのです。AdaCoreの資料は証明できない原因として、コードの誤りのほかに、ループ不変条件のような注釈の不足や、証明器の時間切れなどを挙げています⁶。might fail は誤りがあるという断定ではありません。

ループの各回の終わりに、「ここまでの要素は Key ではない」というループ不変条件を書きます。

      for I in A'Range loop
         if A (I) = Key then
            return I;
         end if;
         pragma Loop_Invariant (for all J in A'First .. I => A (J) /= Key);
      end loop;

GNATproveはループ不変条件が最初の回で成り立つことと、前の回で成り立てば次の回でも成り立つことを確かめます⁷。これで事後条件まで証明できました。(10, 20, 30, 20) から20と99を探し、空の配列から1を探すと、結果は 2、0、0 でした。

flowchart TB
        accTitle: ループ不変条件と事後条件
        accDescr: ループ不変条件がないと見つからなかった場合の事後条件が証明できず、ここまでの要素はKeyではないという不変条件を書くと事後条件まで証明できることを示す。
        A["for ループで先頭から比べる"] --> B["不変条件なし"]
        A --> C["不変条件あり"]
        B --> D["見つからない場合の Post が未証明"]
        C --> E["各回でここまでの要素は Key でない"]
        E --> F["Post まで証明済み"]

図6: ループ不変条件はループの後で成り立つことを証明器に伝える。

while ループで書いた場合

同じ探索を、添字を自分で1つずつ進める while ループで書くと、3つのメッセージが出ました。

   function Find (A : Int_Array; Key : Integer) return Natural is
      I : Positive := A'First;
   begin
      while I <= A'Last loop
         pragma Loop_Invariant (I in A'Range);
         pragma Loop_Invariant (for all J in A'First .. I - 1 => A (J) /= Key);
         if A (I) = Key then
            return I;
         end if;
         I := I + 1;
      end loop;
      return 0;
   end Find;

search.adb:4:24: medium: range check might fail, cannot prove lower bound for A'First
    4 |      I : Positive := A'First;
      |                      ~^~~~~~
  reason for check: default component value must fit in the type

search.adb:6:25: medium: implicit aspect Always_Terminates on "Find" could be incorrect, loop might be nonterminating
    6 |      while I <= A'Last loop
      |                        ^~~~
  possible fix: add loop variant in the loop body

search.adb:12:17: medium: overflow check might fail, cannot prove upper bound for I + 1
   12 |         I := I + 1;
      |              ~~^~~
  reason for check: result of addition must fit in a 32-bits machine integer

1つ目は空の配列の下限です。Adaでは、空の範囲は添字の型の範囲に入っていなくてもかまいません⁸。そのため、空の配列の A'First が Positive に入るとは限りません。3つ目は A'Last が Integer'Last の配列で、最後の要素を調べた後の I + 1 があふれることを指しています。2つ目はループが終わることを示せないという指摘です。GNATproveは関数が必ず終わることも既定で確かめます⁹。

for ループで書けば、添字の範囲を言語が決めるので、この3つはどれも出ませんでした。

証明が保証することとしないこと

ここまでの結果を整理します。GNATproveが「すべて証明済み」と言ったとき、確かめられているのは、事前条件を満たすすべての入力について、SPARKの範囲の本体で実行時エラーが起きず、事後条件が成り立つことです。テストのように入力を選んだ結果ではありません。

一方で、次のことは確かめていません。

• 契約が仕様どおりか。Clamp の弱い事後条件や、平均の丸め方の例がこれに当たります。
• SPARKの解析対象でないコードが契約を守るか。呼び出し側が事前条件を守ること、呼ばれる側が契約どおりに動くことは、前提として扱われます⁴。
• 人が「成り立つ」と宣言した事柄。次の節の pragma Assume と pragma Annotate がこれに当たります。
• メモリ不足。AdaCoreの資料はスタックとヒープの大きさを別に確かめるべき前提に挙げています⁴。

flowchart TB
        accTitle: 証明が確かめる範囲
        accDescr: GNATproveが確かめるのは本体が契約を満たし実行時エラーが起きないことで、契約が仕様どおりか、解析対象外のコード、AssumeやAnnotateで宣言した事柄、メモリ不足は確かめないことを示す。
        A["GNATproveの証明"] --> B["確かめる"]
        A --> C["確かめない"]
        B --> D["実行時エラーが起きない"]
        D ~~~ E["本体が Post を満たす"]
        C --> F["契約が仕様どおりか"]
        F ~~~ G["解析対象外のコード"]
        G ~~~ H["Assume と Annotate の中身"]
        H ~~~ I["メモリ不足"]

図7: 証明が確かめることと、前提として扱うこと。

証明の失敗を表示から消す書き方

失敗した証明はコードを直さなくても表示から消せます。AIに「GNATproveのエラーをなくして」とだけ頼んだときは、差分にこうした行が入っていないかを確かめます。最初の (A + B) / 2 の本体で、3通り試しました。

pragma Assume

本体の先頭に pragma Assume (A in -1_000 .. 1_000 and B in -1_000 .. 1_000); を書くと、--report=fail の出力は空になりました。pragma Assume はGNATproveに確かめさせずに、その性質が成り立つものとして以降の解析に使わせるプラグマです⁷。ただし gnatprove.out には使った場所が残ります。

  Averages.Average at averages.ads:3 flow analyzed (0 errors, 0 checks, 0 warnings and 1 pragma Assume statements) and proved (3 checks)
   pragma Assume statements:
    averages.adb:5:7

pragma Annotate による正当化

pragma Annotate (GNATprove, False_Positive, "overflow check might fail", "理由") は、検査のメッセージを「誤検知」として正当化します。このプラグマは直前の項目に掛かります。最初に return 文の前に置いたときは、正当化の対象がないという警告が出て、あふれのメッセージはそのまま残りました。足し算を定数の宣言に移し、その直後に置くと、メッセージは info: overflow check justified に変わりました¹⁰。gnatprove.out の表では Justified の列に1と数えられ、理由の文字列も残ります。

   Justified check messages:
    averages.adb:4:35: overflow check justified (marked as: false positive, reason: "A と B は小さい値しか来ない")

SPARK_Mode => Off

本体を package body Averages with SPARK_Mode => Off is にすると、本体は解析されません。出力は warning: no checks generated by GNATprove だけで、gnatprove.out には skipped; body is SPARK_Mode => Off と残りました。

AdaCoreの資料は、検査メッセージの正当化はすべてレビューするべきで、pragma Assume による正当化は慎重に調べるべきだとしています⁴。3つとも使う理由がある場面はあります。問題なのは、理由を確かめないまま差分に入ることです。

flowchart TB
        accTitle: 証明の失敗を表示から消す3つの書き方
        accDescr: pragma Assumeは前提として使われ、pragma Annotateは正当化済みとして数えられ、SPARK_Mode Offは本体が解析されなくなり、どれもgnatprove.outに記録が残ることを示す。
        A["失敗した検査"] --> B["pragma Assume"]
        A --> C["pragma Annotate"]
        A --> D["SPARK_Mode => Off"]
        B --> E["Assume の場所が残る"]
        C --> F["Justified に数えられる"]
        D --> G["skipped と残る"]

図8: どの書き方でも、gnatprove.out に跡が残る。

レビューで人が見る箇所

AIのコードにGNATproveをかける場合、人が読む順は次のとおりです。

1. 事前条件。業務で来る入力を締め出していないか、平均の例の possible fix のように証明を通すためだけに足した条件ではないかを見ます。
2. 事後条件。結果が1つに決まるか、決まらないなら残る幅（丸め方など）が仕様で許されるかを見ます。
3. 差分の中の pragma Assume、pragma Annotate、SPARK_Mode => Off。それぞれに理由があるかを見ます。
4. gnatprove.out の表。Unproved が0か、Justified の件数と理由、pragma Assume の一覧を見ます。

本体を1行ずつ読むのは、その後で足ります。契約が仕様どおりで、前提を置かずにすべて証明できていれば、本体が実行時エラーを起こすことも事後条件に反することもないからです。

flowchart TB
        accTitle: AIのコードをレビューする順序
        accDescr: 事前条件、事後条件、AssumeとAnnotateとSPARK_Mode Offの追加、gnatprove.outの表の順に確かめ、本体はその後に読むことを示す。
        A["Pre: 入力を締め出していないか"] --> B["Post: 結果が決まるか"]
        B --> C["Assume・Annotate・Off の理由"]
        C --> D["Unproved と Justified の件数"]
        D --> E["本体を読む"]

図9: 本体より先に、契約と証明の結果を読む。

テストとの組み合わせ

AdaCoreの資料は、証明した性質はテストしなくてよく、単体テストを減らしたり、なくしたりできるとしています¹。ただし、それは契約が要求を正しく表している場合の話です。AIに契約まで書かせるなら、契約が要求どおりかを確かめる手段としてテストが残ります。Clamp の例で弱い事後条件のまま証明が通った誤りは、具体的な値で実行して期待値と比べれば、すぐに分かるものでした。逆に、普通の値では起きない極端な値でのあふれは、証明が見つけました。

事後条件はどの入力でも成り立つ性質を書いたものなので、プロパティベーステストの性質と同じ形をしています。違いは、テストが多数の入力を試すのに対して、証明はすべての入力について確かめることです。AIが書いたテストの見分け方と、テストの弱さを道具で調べる方法は、次の記事で扱っています。

• AIが書いたテストを信用してよいか
• コードカバレッジでテストされていないコードを見つける
• ミューテーションテストでテストをテストする
• プロパティベーステストで、AIが思いつかない入力を試す

社員の方が生成AIで作ったツールやマクロを、本番で使う前に確かめたい場合は、「AIで作ったコードのプロレビュー・相談」で相談を受けています。

関連記事

• SPARKによる形式検証入門 ── Adaの契約から数学的証明へ
• Ada言語の魅力 ── 型で設計を語り、数十年動き続けるソフトウェアを支える言語
• Ada と C / C# をつなぐ ── DLL を作って呼び出す
• Alire で Ada のプロジェクトを始める

参考リンク

関連する記事

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

関連トピック

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

このテーマがつながるサービス

この記事は次のサービスページにつながります。近い入口からご覧ください。

よくある質問

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

AIが書いたAdaのコードをGNATproveにかけると、何が分かりますか？

SPARKの範囲で書かれたコードについて、オーバーフローや配列の範囲外アクセスのような実行時エラーが起きないことと、事後条件が成り立つことを、事前条件を満たすすべての入力について確かめます。証明できなかった箇所は、行と列、理由、反例の値つきで表示されます。

GNATproveの証明が通れば、レビューは要りませんか？

要ります。証明が確かめるのは本体が契約を満たすことで、契約が仕様どおりかは確かめません。事後条件が弱ければ、誤った本体でも証明は通ります。人は本体よりも、事前条件と事後条件、pragma Assume や pragma Annotate、SPARK_Mode => Off の追加を読みます。

「might fail」と出たら、コードは必ず間違っていますか？

必ずではありません。コードが誤っている場合のほか、ループ不変条件のような注釈が足りない場合や、証明器が時間内に証明できない場合にも出ます。反例の値が付いていれば、その値で実際に誤るかを確かめると原因を絞れます。

GNATproveが提案する事前条件をそのまま足してもよいですか？

証明は通りますが、関数が受け付ける入力が狭まります。条件を満たすことは呼び出し側の責任になるので、その条件が業務上の入力をすべて含むかを人が判断します。含まないなら、本体を直します。

著者プロフィール

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

小村 豪

合同会社小村ソフト 代表

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