知識マップ: SPARKによる形式検証入門 ── Adaの契約から数学的証明へ

記事「SPARKによる形式検証入門 ── Adaの契約から数学的証明へ」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

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件)

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

• SPARKはAda(プログラミング言語)を利用します。SPARKはAdaの言語仕様、特にAda 2012で追加された契約(Pre/Post)機能を土台として作られている / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• SPARKは形式検証の実装を担います。SPARKはAdaのサブセットとして、契約に書いた性質を数学的に証明する形式検証を実装として提供する / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• SPARKは契約による設計(Pre/Post)を前提とします。SPARKの証明のうち、書いた性質の証明はPre/Postで書かれた契約を証明の入力とすることを前提とする。ただしオーバーフロー・範囲外アクセス・ゼロ除算などの実行時エラー不在(AoRTE)の証明は、明示的なPre/Post契約を書かなくても型の範囲制約などから成立し得る / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典
• SPARKはGNATproveを利用します。SPARKコードの検証には、AdaCoreが提供するGNATproveというツールを使う / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• GNATproveはAda(プログラミング言語)を前提とします。GNATproveはGNATツールチェーンに同梱されて提供され、Adaのコンパイル環境を前提とする / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• GNATproveはWhy3を利用します。GNATproveは契約や表明をいったんWhy3の中間言語に変換してから証明器に渡す / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• Why3はSMTソルバ(自動証明器)を利用します。Why3は複数の自動証明器(SMTソルバ)へ証明課題を振り分けるプラットフォームである / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• SPARKはループ不変条件(Loop Invariant)を前提とします。ループを含む性質を証明する場合、SPARKはLoop_Invariantでループの各反復で成り立つ性質を示すことを前提とする / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典
• SPARKはデータフロー契約(Global/Depends)を利用します。SPARKは副作用を管理するため、Global/Depends契約でグローバル変数の読み書きと依存関係を明示する / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• SPARKは証明レベル(Stone〜Platinum)を利用します。SPARKは証明の厳しさをStoneからPlatinumまで段階的に定義する証明レベルの考え方を使う / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• SPARKはRavenscarプロファイルを前提とします。SPARKでタスクを扱う場合、並行処理をRavenscar(または後継のJorvik)プロファイルの範囲に限定することを前提とする / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典
• Ada(プログラミング言語)はAlireで構成できます。GNATツールチェーンを使う場合、Ada/SPARKはAlireというソースベースのパッケージマネージャーで導入・構成できる / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典
• AUnitはSPARKに対する本記事の推奨です。SPARKで型と契約を固めたうえでAUnitによる単体テストを組み合わせることが実践的な運用として推奨される / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• Silverレベル(AoRTE)はSPARKに対する本記事の推奨です。実行時エラーが起きないことを証明するSilverレベルは、SPARK導入における実務上の既定の目標として推奨される / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• Silverレベル(AoRTE)はGNATproveで確認できます。Silverレベルが達成されている(範囲外・オーバーフロー・ゼロ除算が起きない)ことはGNATproveの証明で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• データフロー契約(Global/Depends)はGNATproveで確認できます。Global/Depends契約が意図通りであることはGNATproveのフロー解析(Bronzeレベル)で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• 契約による設計(Pre/Post)はGNATproveで確認できます。Pre/Post契約が満たされることはGNATproveの証明で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典

主要概念の定義

SPARK

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

形式検証

プログラムがすべての入力に対してある性質を満たすことを数学的に証明する、テストとは異なる品質保証の手法である。

GNATprove

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

Why3

演繹的プログラム検証のための中間言語とプラットフォームで、証明課題を複数の自動証明器へ振り分ける。

Ada(プログラミング言語)

1970年代後半にアメリカ国防総省の主導で標準化された、強い型付けと高信頼性を重視する汎用プログラミング言語。最新標準はAda 2022。

AUnit

Adaの単体テストフレームワークで、SPARKで証明できなかった部分の振る舞いをテストする用途で併用される。

Silverレベル(AoRTE)

範囲外アクセス・オーバーフロー・ゼロ除算などの実行時エラーが起きないことを証明する、証明レベルのうち実務上の既定目標とされる段階である。

データフロー契約(Global/Depends)

サブプログラムが読み書きするグローバル変数と、変数間の依存関係を宣言するSPARKの契約である。

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

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

機械可読データ

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

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