@prefix schema: <https://schema.org/> .
@prefix skos: <http://www.w3.org/2004/02/skos/core#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix ks: <https://comcomponent.com/vocab/> .

<https://comcomponent.com/blog/ada-spark-image-processing-proof/#article>
    schema:about <https://comcomponent.com/knowledge/spark-silver-level/>, <https://comcomponent.com/knowledge/spark/> ;
    schema:mentions <https://comcomponent.com/knowledge/gnatprove/>, <https://comcomponent.com/knowledge/buffer-overrun/>, <https://comcomponent.com/knowledge/integer-overflow/>, <https://comcomponent.com/knowledge/design-by-contract/>, <https://comcomponent.com/knowledge/loop-invariant/>, <https://comcomponent.com/knowledge/ada-range-constraint/>, <https://comcomponent.com/knowledge/connected-component-labeling/>, <https://comcomponent.com/knowledge/ada-pragma-suppress/>, <https://comcomponent.com/knowledge/auto-vectorization/>, <https://comcomponent.com/knowledge/gnat/> .

<https://comcomponent.com/knowledge/spark-silver-level/> a skos:Concept ;
    skos:prefLabel "Silverレベル(AoRTE)"@ja ;
    skos:definition "範囲外アクセス・オーバーフロー・ゼロ除算などの実行時エラーが起きないことを証明する、証明レベルのうち実務上の既定目標とされる段階である。"@ja ;
    skos:altLabel "Absence of Run-time Errors" ;
    skos:altLabel "AoRTE" ;
    skos:broader <https://comcomponent.com/knowledge/spark-proof-level/> ;
    ks:verifiedBy <https://comcomponent.com/knowledge/gnatprove/> ;
    ks:prevents <https://comcomponent.com/knowledge/buffer-overrun/> ;
    ks:prevents <https://comcomponent.com/knowledge/integer-overflow/> ;
    ks:shouldPrecede <https://comcomponent.com/knowledge/ada-pragma-suppress/> .

<https://comcomponent.com/knowledge/spark/> a skos:Concept ;
    skos:prefLabel "SPARK"@ja ;
    skos:definition "プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。"@ja ;
    skos:altLabel "SPARK Ada" ;
    skos:altLabel "GNATprove" ;
    ks:uses <https://comcomponent.com/knowledge/gnatprove/> .

<https://comcomponent.com/knowledge/gnatprove/> a skos:Concept ;
    skos:prefLabel "GNATprove"@ja ;
    skos:definition "AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。"@ja ;
    skos:altLabel "gnatprove コマンド"@ja ;
    skos:broader <https://comcomponent.com/knowledge/spark/> .

<https://comcomponent.com/knowledge/buffer-overrun/> a skos:Concept ;
    skos:prefLabel "バッファオーバーラン"@ja ;
    skos:definition "配列やバッファの範囲外への書き込み・読み込みが起こる現象。C/C++で長年セキュリティ脆弱性の主要原因とされてきた。"@ja ;
    skos:altLabel "buffer overrun" ;
    skos:altLabel "buffer overflow" .

<https://comcomponent.com/knowledge/integer-overflow/> a skos:Concept ;
    skos:prefLabel "整数オーバーフロー"@ja ;
    skos:definition "整数の演算結果が、その型で表せる範囲を超えること。言語と設定によって、例外・パニック・折り返しのいずれかになる。Adaでは、値が型の基本範囲に収まるかを確かめるOverflow_Checkに失敗すると、実行時にConstraint_Errorが送出される。"@ja ;
    skos:altLabel "Integer Overflow" ;
    skos:altLabel "integer overflow" ;
    skos:altLabel "算術オーバーフロー"@ja ;
    skos:altLabel "Overflow_Check" .

<https://comcomponent.com/knowledge/design-by-contract/> a skos:Concept ;
    skos:prefLabel "契約による設計(Pre/Post)"@ja ;
    skos:definition "サブプログラムの入口での前提条件(Pre)と、出口で保証する性質(Post)を宣言的に記述する、Ada 2012の契約機構である。"@ja ;
    skos:altLabel "Design by Contract" ;
    skos:altLabel "事前条件・事後条件"@ja ;
    skos:broader <https://comcomponent.com/knowledge/ada/> .

<https://comcomponent.com/knowledge/loop-invariant/> a skos:Concept ;
    skos:prefLabel "ループ不変条件(Loop Invariant)"@ja ;
    skos:definition "ループの各反復の開始時点で成り立つ性質を宣言し、ループに関する性質の証明を可能にするSPARKのプラグマである。"@ja ;
    skos:altLabel "Loop_Invariant" ;
    skos:broader <https://comcomponent.com/knowledge/spark/> .

<https://comcomponent.com/knowledge/connected-component-labeling/> a skos:Concept ;
    skos:prefLabel "連結成分のラベリング"@ja ;
    skos:definition "2値画像で、隣り合ってつながった前景の画素の塊（連結成分）ごとに異なる番号（ラベル）を付ける画像処理。画像を2回走査し、1回目で仮のラベルとラベルどうしの対応を記録し、2回目でまとめる方法がよく使われる。"@ja ;
    skos:altLabel "Connected-component labeling" ;
    skos:altLabel "ラベリング処理"@ja .

<https://comcomponent.com/knowledge/ada-range-constraint/> a skos:Concept ;
    skos:prefLabel "範囲制約(range constraint)"@ja ;
    skos:definition "型に値の範囲を持たせ、違反を実行時にConstraint_Error例外として検出するAdaの仕組み。配列アクセスの境界チェックにも使われる。"@ja ;
    skos:altLabel "subtype" ;
    skos:altLabel "Constraint_Error" ;
    ks:mitigates <https://comcomponent.com/knowledge/buffer-overrun/> .

<https://comcomponent.com/knowledge/ada-pragma-suppress/> a skos:Concept ;
    skos:prefLabel "pragma Suppress"@ja ;
    skos:definition "指定した種類の言語定義の実行時検査を外してよいことをコンパイラーに許すAdaのプラグマ。外した検査が失敗する状況が起きると、実行は誤り（erroneous）になる。GNATの-gnatpは、ユニット全体にpragma Suppress (All_Checks)を書いたのと同じ扱いになる。"@ja ;
    skos:altLabel "Suppress(All_Checks)" ;
    skos:altLabel "検査の抑止"@ja .

<https://comcomponent.com/knowledge/gnat/> a skos:Concept ;
    skos:prefLabel "GNAT"@ja ;
    skos:definition "GCCに含まれる無償のAdaコンパイラで、Adaの代表的な処理系。"@ja ;
    skos:altLabel "GNATコンパイラ"@ja .

<https://comcomponent.com/knowledge/auto-vectorization/> a skos:Concept ;
    skos:prefLabel "自動ベクトル化"@ja ;
    skos:definition "コンパイラーがループを解析し、複数のデータを1命令で処理するSIMD命令を使うコードに自動で書き換える最適化。GCCではGCC 12から-O2で有効になるが、コストモデルによって、データの重なりを実行時に確かめる必要があるループを対象にするかが変わる。"@ja ;
    skos:altLabel "Auto-vectorization" ;
    skos:altLabel "ループのベクトル化"@ja ;
    skos:altLabel "-ftree-vectorize" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "SPARKで書いた画像処理のコードの検査と契約を、GNATproveで証明する。この記事では gnatprove -P img_proof.gpr -j0 --level=2 --report=all で実行した"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_view_gnatprove_output.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark-silver-level/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "実行時エラーがないこと（SPARK silver）をGNATproveで証明できる。記事では2値化、3×3の平滑化、連結成分のラベリングで、添字・範囲・あふれの検査が事前条件を満たすどの入力でも失敗しないことを証明した"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#spark-silver-absence-of-run-time-errors-aorte> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark-silver-level/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/buffer-overrun/> ;
    schema:description "SPARKのユーザーガイドは、Silverの効果として、バッファオーバーフローを突いて制御の流れを乗っ取られないことを挙げている。画像処理では、近傍を読む処理の端、行と列の取り違え、画素から求めた値を表の添字に使う処理で画像の外へのアクセスが起きやすい"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#spark-silver-absence-of-run-time-errors-aorte> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark-silver-level/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/integer-overflow/> ;
    schema:description "Silverでは整数のオーバーフローも起きないことを証明する。記事の平滑化では、9つの画素の合計がNaturalであふれないことと、9で割った結果が画素の型に収まることが証明された"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#spark-silver-absence-of-run-time-errors-aorte> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark-silver-level/> ;
    rdf:predicate ks:requires ;
    rdf:object <https://comcomponent.com/knowledge/design-by-contract/> ;
    schema:description "出力画像の添字の検査を証明するには、入力と出力の行と列の範囲が等しいという事前条件が要る。平滑化では、空の画像の範囲の境界は添字の型の外にありうるので、画像が空でないことも事前条件に書いた。GNATproveは本体を証明するときに事前条件を仮定し、SPARKの呼び出し側では呼ぶたびに事前条件を証明する。SPARKではない呼び出し側からは事前条件を実行時に検査するよう勧められており、記事では証明したユニットの仕様にpragma Assertion_Policy (Pre => Check)を書き、検査を外したビルドでも事前条件を検査した"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/subprogram_contracts.html#preconditions>, <https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#choosing-which-run-time-checking-to-keep>, <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-5.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/design-by-contract/> ;
    rdf:predicate ks:requires ;
    rdf:object <https://comcomponent.com/knowledge/loop-invariant/> ;
    schema:description "事後条件を証明する場合の関係。ループで出力画像を埋める2値化の事後条件を証明するには、書き終えた範囲を表すループ不変条件と、書き換えていない部分が変わらないこと（frame condition）が要る。画像の外にアクセスしないことの証明だけなら、ループ不変条件は要らなかった"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_write_loop_invariants.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/connected-component-labeling/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "2回の走査によるラベリングで実行時エラーがないことをGNATproveで証明した。対応表の添字と要素を同じ型にすると、代表を探すループは不変条件なしで証明できる。仮ラベルの数が上限を超える場合は失敗を返す。結果の正しさ、代表を探す処理の終了、仮ラベルの数が上限を超えないことは証明しておらず、結果はテスト、乱数の画像での塗りつぶしとの比較、Cの実装との比較で確かめた"@ja ;
    ks:evidence <https://doi.org/10.1145/321356.321357>, <https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_write_subprogram_contracts.html#subprogram-termination> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-range-constraint/> ;
    rdf:predicate ks:mitigates ;
    rdf:object <https://comcomponent.com/knowledge/buffer-overrun/> ;
    schema:description "Adaでは添字の検査が実行時に働くので、画像の外へのアクセスはほかのメモリを読み書きせずConstraint_Errorになる。ただし装置の上で例外が出れば、処理はそこで止まる"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-11-5.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-pragma-suppress/> ;
    rdf:predicate ks:mayCause ;
    rdf:object <https://comcomponent.com/knowledge/buffer-overrun/> ;
    schema:description "検査を外した状態で、その検査が失敗する状況が起きると、実行は誤り（erroneous）になる。証明していないコードで添字の検査を外すと、画像の外へのアクセスが何を引き起こすか分からなくなる"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-11-5.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark-silver-level/> ;
    rdf:predicate ks:shouldPrecede ;
    rdf:object <https://comcomponent.com/knowledge/ada-pragma-suppress/> ;
    schema:description "SPARKのユーザーガイドは、プログラム全体で検査を外すのではなく、GNATproveで実行時エラーがないことを証明した部分だけ検査を外す方法を勧めている。記事ではgprbuildでファイルごとに-gnatpを付け、証明できたユニットだけ検査を外した"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#safe-optimization-of-run-time-checks> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/gnat/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/auto-vectorization/> ;
    schema:description "GNATでコンパイルしたAdaのループもGCCの自動ベクトル化の対象になる。記事の測定（GCC 13.3.0）では、-O2のvery-cheapのコストモデルでは2値化と平滑化のループがベクトル化されなかった（検査を残した平滑化はループの中の検査の分岐が理由）。-O3ではdynamicのコストモデルとループのアンスイッチングにより、検査を残したままでもベクトル化されて、Cと同じ速さになった"@ja ;
    ks:evidence <https://gcc.gnu.org/onlinedocs/gcc/Optimize-Options.html>, <https://gcc.gnu.org/gcc-12/changes.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "context-dependent" .