知識マップ: 画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較

記事「画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

画像処理のコードが画像の外を読み書きしないことを、SPARKのGNATproveで証明する。2値化は画像の型と、入力と出力の範囲が等しいという事前条件で、3×3の平滑化はそれに加えて画像が空でないという事前条件で、実行時エラーがないこと（Silver）を証明できる。2値化の事後条件にはループ不変条件が要る。連結成分のラベリングは、対応表の添字と要素を同じ型にすると実行時エラーがないことを証明できるが、結果の正しさはテストで確かめた。証明できたユニットだけpragma Suppress（-gnatp）で検査を外すと、-O2ではCとほぼ同じ速さになった。-O3ではGCCの自動ベクトル化が働き、2値化と平滑化は検査を残してもCと同じ速さになった。

flowchart LR
    accTitle: 画像処理の境界外アクセスをSPARKで証明する記事の知識マップ
    accDescr: SPARKのSilver（実行時エラーがないこと）をGNATproveで証明するとバッファオーバーランと整数オーバーフローを防げること、その証明には事前条件が要り、事後条件にはループ不変条件が要ること、連結成分のラベリングの実行時エラーがないこともGNATproveで確かめられること、証明をpragma Suppressで検査を外すより先に行うこと、Adaの添字の検査と自動ベクトル化との関係を示す図。
    spark_silver_level["Silverレベル(AoRTE)"]
    spark["SPARK"]
    gnatprove["GNATprove"]
    buffer_overrun["バッファオーバーラン"]
    integer_overflow["整数オーバーフロー"]
    design_by_contract["契約による設計(Pre/Post)"]
    loop_invariant["ループ不変条件(Loop Invariant)"]
    connected_component_labeling["連結成分のラベリング"]
    ada_range_constraint["範囲制約(range constraint)"]
    ada_pragma_suppress["pragma Suppress"]
    gnat["GNAT"]
    auto_vectorization["自動ベクトル化"]
    spark -->|"利用する"| gnatprove
    spark_silver_level -->|"で確認できる"| gnatprove
    spark_silver_level -->|"防止する"| buffer_overrun
    spark_silver_level -->|"防止する"| integer_overflow
    spark_silver_level -.->|"前提とする"| design_by_contract
    design_by_contract -.->|"前提とする"| loop_invariant
    connected_component_labeling -.->|"で確認できる"| gnatprove
    ada_range_constraint -->|"軽減する"| buffer_overrun
    ada_pragma_suppress -.->|"原因になり得る"| buffer_overrun
    spark_silver_level -->|"より先に行うべき"| ada_pragma_suppress
    gnat -.->|"利用する"| auto_vectorization

概念間の関係(全11件)

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

• SPARKはGNATproveを利用します。SPARKで書いた画像処理のコードの検査と契約を、GNATproveで証明する。この記事では gnatprove -P img_proof.gpr -j0 --level=2 --report=all で実行した / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• Silverレベル(AoRTE)はGNATproveで確認できます。実行時エラーがないこと（SPARK silver）をGNATproveで証明できる。記事では2値化、3×3の平滑化、連結成分のラベリングで、添字・範囲・あふれの検査が事前条件を満たすどの入力でも失敗しないことを証明した / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• Silverレベル(AoRTE)はバッファオーバーランを防ぎます。SPARKのユーザーガイドは、Silverの効果として、バッファオーバーフローを突いて制御の流れを乗っ取られないことを挙げている。画像処理では、近傍を読む処理の端、行と列の取り違え、画素から求めた値を表の添字に使う処理で画像の外へのアクセスが起きやすい / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• Silverレベル(AoRTE)は整数オーバーフローを防ぎます。Silverでは整数のオーバーフローも起きないことを証明する。記事の平滑化では、9つの画素の合計がNaturalであふれないことと、9で割った結果が画素の型に収まることが証明された / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• Silverレベル(AoRTE)は契約による設計(Pre/Post)を前提とします。出力画像の添字の検査を証明するには、入力と出力の行と列の範囲が等しいという事前条件が要る。平滑化では、空の画像の範囲の境界は添字の型の外にありうるので、画像が空でないことも事前条件に書いた。GNATproveは本体を証明するときに事前条件を仮定し、SPARKの呼び出し側では呼ぶたびに事前条件を証明する。SPARKではない呼び出し側からは事前条件を実行時に検査するよう勧められており、記事では証明したユニットの仕様にpragma Assertion_Policy (Pre => Check)を書き、検査を外したビルドでも事前条件を検査した / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典 出典 出典
• 契約による設計(Pre/Post)はループ不変条件(Loop Invariant)を前提とします。事後条件を証明する場合の関係。ループで出力画像を埋める2値化の事後条件を証明するには、書き終えた範囲を表すループ不変条件と、書き換えていない部分が変わらないこと（frame condition）が要る。画像の外にアクセスしないことの証明だけなら、ループ不変条件は要らなかった / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
• 連結成分のラベリングはGNATproveで確認できます。2回の走査によるラベリングで実行時エラーがないことをGNATproveで証明した。対応表の添字と要素を同じ型にすると、代表を探すループは不変条件なしで証明できる。仮ラベルの数が上限を超える場合は失敗を返す。結果の正しさ、代表を探す処理の終了、仮ラベルの数が上限を超えないことは証明しておらず、結果はテスト、乱数の画像での塗りつぶしとの比較、Cの実装との比較で確かめた / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典 出典
• 範囲制約(range constraint)はバッファオーバーランを軽減します。Adaでは添字の検査が実行時に働くので、画像の外へのアクセスはほかのメモリを読み書きせずConstraint_Errorになる。ただし装置の上で例外が出れば、処理はそこで止まる / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• pragma Suppressはバッファオーバーランの原因になることがあります。検査を外した状態で、その検査が失敗する状況が起きると、実行は誤り（erroneous）になる。証明していないコードで添字の検査を外すと、画像の外へのアクセスが何を引き起こすか分からなくなる / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
• Silverレベル(AoRTE)はpragma Suppressより先に行うべきです。SPARKのユーザーガイドは、プログラム全体で検査を外すのではなく、GNATproveで実行時エラーがないことを証明した部分だけ検査を外す方法を勧めている。記事ではgprbuildでファイルごとに-gnatpを付け、証明できたユニットだけ検査を外した / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• GNATは自動ベクトル化を利用します。GNATでコンパイルしたAdaのループもGCCの自動ベクトル化の対象になる。記事の測定（GCC 13.3.0）では、-O2のvery-cheapのコストモデルでは2値化と平滑化のループがベクトル化されなかった（検査を残した平滑化はループの中の検査の分岐が理由）。-O3ではdynamicのコストモデルとループのアンスイッチングにより、検査を残したままでもベクトル化されて、Cと同じ速さになった / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典 出典

主要概念の定義

Silverレベル(AoRTE)

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

SPARK

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

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

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

連結成分のラベリング

2値画像で、隣り合ってつながった前景の画素の塊（連結成分）ごとに異なる番号（ラベル）を付ける画像処理。画像を2回走査し、1回目で仮のラベルとラベルどうしの対応を記録し、2回目でまとめる方法がよく使われる。

範囲制約(range constraint)

型に値の範囲を持たせ、違反を実行時にConstraint_Error例外として検出するAdaの仕組み。配列アクセスの境界チェックにも使われる。

pragma Suppress

指定した種類の言語定義の実行時検査を外してよいことをコンパイラーに許すAdaのプラグマ。外した検査が失敗する状況が起きると、実行は誤り（erroneous）になる。GNATの-gnatpは、ユニット全体にpragma Suppress (All_Checks)を書いたのと同じ扱いになる。

GNAT

GCCに含まれる無償のAdaコンパイラで、Adaの代表的な処理系。

機械可読データ

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

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

作成

合同会社小村ソフト

ライセンス

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

最終確認日

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

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