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

記事「AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

AIが書いたAdaの関数に、人が事前条件と事後条件を書き、SPARKのGNATproveで証明する。GNATproveは整数オーバーフローのような実行時エラーと事後条件の違反を、反例の値つきで報告する。ループを含む事後条件の証明にはループ不変条件が要る。証明が確かめるのは本体が契約を満たすことだけなので、人のコードレビューでは契約と、pragma Assume・pragma Annotate・SPARK_Mode => Offの追加を先に読む。弱い契約のまま通った誤りは、具体的な期待値を書いたユニットテストで見つかる。

flowchart LR
    accTitle: AIが書いたコードをSPARKで証明する記事の知識マップ
    accDescr: GNATproveが契約と整数オーバーフローを確かめ、ループ不変条件が証明に要ること、pragma Assumeとpragma AnnotateとSPARK_Modeが証明の対象を変えるのでコードレビューで確かめること、証明と併せてユニットテストを使うことを示す図。
    spark["SPARK"]
    design_by_contract["契約による設計(Pre/Post)"]
    formal_verification["形式検証"]
    gnatprove["GNATprove"]
    integer_overflow["整数オーバーフロー"]
    loop_invariant["ループ不変条件(Loop Invariant)"]
    spark_pragma_assume["pragma Assume"]
    spark_pragma_annotate["pragma Annotate(GNATprove)"]
    spark_mode["SPARK_Mode"]
    code_review["コードレビュー(プルリクエストレビュー)"]
    unit_test["ユニットテスト"]
    spark -->|"実装を担う"| formal_verification
    spark -->|"利用する"| gnatprove
    design_by_contract -->|"で確認できる"| gnatprove
    integer_overflow -->|"で確認できる"| gnatprove
    spark -.->|"前提とする"| loop_invariant
    gnatprove -->|"利用する"| spark_pragma_assume
    gnatprove -->|"利用する"| spark_pragma_annotate
    gnatprove -->|"で構成できる"| spark_mode
    code_review -->|"推奨される対応"| design_by_contract
    code_review -->|"推奨される対応"| spark_pragma_assume
    code_review -->|"推奨される対応"| spark_pragma_annotate
    unit_test -.->|"推奨される対応"| formal_verification

概念間の関係(全12件)

図と同じ関係を文章でも列挙します。表示している文と機械可読な意味データ(RDFa)は同じ要素に載っています。確度が「確立した関係」のものは直接の関係として、「条件付きの関係」のものは成立条件つきの言明(rdf:Statement)として表現しています。

• SPARKは形式検証の実装を担います。SPARKはAdaのサブセットとして、契約に書いた性質を数学的に証明する形式検証を提供する / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• SPARKはGNATproveを利用します。SPARKのコードの証明にはGNATproveを使う。この記事では gnatprove -P p.gpr --level=2 --report=fail で実行した / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• 契約による設計(Pre/Post)はGNATproveで確認できます。事前条件を満たすすべての入力について事後条件が成り立つことを、GNATproveで確かめられる。確かめるのは本体が契約を満たすことで、契約が仕様どおりかは確かめない / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• 整数オーバーフローはGNATproveで確認できます。SPARKの範囲の本体で整数の演算があふれ得る箇所を、GNATproveが overflow check might fail として反例の値つきで報告する。反例は実行できる入力に対応するとは限らない / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• SPARKはループ不変条件(Loop Invariant)を前提とします。ループの後で成り立つ事後条件を証明するには、Loop_Invariantでループの各回で成り立つ性質を示す必要がある。本体が正しくても、不変条件がないと証明できないことがある / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典 出典
• GNATproveはpragma Assumeを利用します。GNATproveはpragma Assumeの性質を確かめずに、以降の解析の前提として使う。使った場所は gnatprove.out に一覧される / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• GNATproveはpragma Annotate(GNATprove)を利用します。GNATproveはpragma Annotateで正当化された検査メッセージを、失敗ではなく正当化済みとして扱い、理由を解析結果の記録に残す / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• GNATproveはSPARK_Modeで構成できます。GNATproveが解析する範囲はSPARK_Modeで決まり、SPARK_Mode => Offにした本体は解析されない / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• コードレビュー(プルリクエストレビュー)は契約による設計(Pre/Post)に対する本記事の推奨です。AIが書いたコードを証明する場合、人は本体より先に、事前条件が業務上の入力を締め出していないかと、事後条件が結果を決め切っているかを読む / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• コードレビュー(プルリクエストレビュー)はpragma Assumeに対する本記事の推奨です。pragma Assumeは確かめられずに前提として使われるので、追加されたら理由をレビューで確かめる / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• コードレビュー(プルリクエストレビュー)はpragma Annotate(GNATprove)に対する本記事の推奨です。検査メッセージの正当化はすべてレビューする。誤った正当化は、実際に失敗し得る検査を隠す / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• ユニットテストは形式検証に対する本記事の推奨です。事後条件が弱いと誤った本体でも証明が通るため、具体的な期待値を書いたユニットテストを証明と併せて使う。記事の例では、常に下限を返す本体が証明を通り、具体的な値で実行すると誤りが分かった / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典

主要概念の定義

SPARK

プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。

契約による設計(Pre/Post)

サブプログラムの入口での前提条件(Pre)と、出口で保証する性質(Post)を宣言的に記述する、Ada 2012の契約機構である。

整数オーバーフロー

整数の演算結果が、その型で表せる範囲を超えること。言語と設定によって、例外・パニック・折り返しのいずれかになる。Adaでは、値が型の基本範囲に収まるかを確かめるOverflow_Checkに失敗すると、実行時にConstraint_Errorが送出される。

GNATprove

AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。

コードレビュー(プルリクエストレビュー)

プルリクエスト単位でコードの変更内容を他者が確認する開発プロセスである。

ユニットテスト

分離された1責務の正しさを、外部資源を切り離して確かめるテストの層のこと。

機械可読データ

• JSON-LD / Turtle ── この記事の知識グラフ全体
• 概念一覧 / 語彙(述語)の定義

このデータセットについて

作成

合同会社小村ソフト

ライセンス

CC BY 4.0 ── 出典(合同会社小村ソフト)とライセンスへのリンクを明示し、改変した場合はその旨を示すことを条件に、再配布・改変を含めて再利用できます

最終確認日

2026-11-01 ── 収録する関係のうち、最後に出典と照合した日

このページはサイトの知識グラフ(_data/knowledge/)から自動生成されています。誤りの指摘はお問い合わせからお願いします。