知識マップ: Adaの検査ロジックをC#の検査アプリから呼ぶ ── 画像バッファをコピーせずに渡し、境界で守る

記事「Adaの検査ロジックをC#の検査アプリから呼ぶ ── 画像バッファをコピーせずに渡し、境界で守る」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

WPFの検査アプリの合否の判定だけをAdaのDLLにし、C#とAdaの間にはC ABIを挟む。C#はLibraryImportによるP/Invokeで関数を呼び、画像のバッファはfixed文でピン留めして先頭のポインター、長さ、幅・高さ・strideを渡す。パラメーターと結果はStructLayoutのSequentialを付けたblittable型の構造体で、大きさを両側で比べてから使う。呼び出し規約はCdeclに合わせる。Adaの境界の関数は寸法を確かめてから同じメモリを配列として見て、SPARK_Modeを付けた判定の関数を呼ぶ。判定の関数の契約とオーバーフローの不在は、ループ不変条件を付けてGNATproveで証明する。境界の関数はAdaの例外をエラーコードに変え、未処理例外としてC#へ出さない。ライブラリはGPRbuildでスタンドアロンライブラリとして作り、自動でエラボレーションを行う。WindowsではDLLになり、GNATのランタイムのDLLとともにアプリのフォルダーに置く。WPFの画面ではUI要素を作ったスレッドから結果を表示する。

flowchart LR
    accTitle: Adaの検査ロジックをC#から呼ぶ記事の知識マップ
    accDescr: AdaとCの相互運用がC ABIを使い、C#からはLibraryImportによるP/Invokeでfixed文でピン留めした画像とblittable型の構造体を渡すこと、判定の関数をSPARKとGNATproveで証明すること、スタンドアロンライブラリがエラボレーションを自動で行いWindowsではDLLになること、例外を境界で止めることを示す図。
    ada_c_interop["AdaとC/C++の相互運用(Annex B)"]
    p_invoke["P/Invoke"]
    c_abi["C ABI(Application Binary Interface)"]
    libraryimport["LibraryImport"]
    csharp_fixed_statement["fixed文(C#)"]
    blittable_type["blittable型"]
    structlayout["StructLayout"]
    calling_convention["呼び出し規約(calling convention)"]
    dll["DLL(ダイナミックリンクライブラリ)"]
    spark["SPARK"]
    gnatprove["GNATprove"]
    spark_mode["SPARK_Mode"]
    design_by_contract["契約による設計(Pre/Post)"]
    integer_overflow["整数オーバーフロー"]
    unhandled_exception["未処理例外"]
    ada_stand_alone_library["スタンドアロンライブラリ(Stand-alone Library)"]
    gprbuild["GPRbuild"]
    ada_elaboration["エラボレーション(elaboration)"]
    ada_task["Adaのタスク(並行処理)"]
    dll_search_order["DLLの検索順序"]
    wpf["WPF"]
    ui_thread_context["UIスレッドのコンテキスト"]
    ada_c_interop -->|"利用する"| c_abi
    libraryimport -->|"実装を担う"| p_invoke
    p_invoke -->|"利用する"| csharp_fixed_statement
    p_invoke -->|"利用する"| blittable_type
    blittable_type -.->|"で構成できる"| structlayout
    p_invoke -->|"前提とする"| calling_convention
    p_invoke -->|"利用する"| dll
    spark -->|"利用する"| gnatprove
    gnatprove -->|"で構成できる"| spark_mode
    design_by_contract -->|"で確認できる"| gnatprove
    integer_overflow -->|"で確認できる"| gnatprove
    ada_c_interop -.->|"原因になり得る"| unhandled_exception
    ada_stand_alone_library -->|"で構成できる"| gprbuild
    ada_stand_alone_library -.->|"自動化する"| ada_elaboration
    ada_task -.->|"両立しない"| ada_stand_alone_library
    ada_stand_alone_library -.->|"利用する"| dll
    dll -.->|"前提とする"| dll_search_order
    wpf -->|"前提とする"| ui_thread_context

概念間の関係(全18件)

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

AdaとC/C++の相互運用(Annex B)はC ABI(Application Binary Interface)を利用します。C#とAdaの間にはC ABI(関数の呼び方と構造体の並びの決まり)を挟む。Convention => Cを付けたレコードはCの構造体に対応し、レコード型のパラメーターとアクセス型のinのパラメーターはCの関数にt*として渡る。記事の例では、NULLを確かめるためにパラメーターと結果をアクセス型で受けた。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
LibraryImportはP/Invokeの実装を担います。記事のC#の層は、LibraryImportでAdaのDLLの関数を宣言し、画像と構造体をポインターで渡す。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
P/Invokeはfixed文(C#)を利用します。画像のバッファはfixed文でReadOnlySpanをピン留めし、先頭のポインターと長さを渡す。fixed文の間はガベージコレクターが配列を動かさず、ポインターはその中でだけ使えるので、Adaは呼び出しの間だけ読み、ポインターを保存しない。空のSpanをピン留めするとポインターはNULLになる。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典出典
P/Invokeはblittable型を利用します。記事のパラメーターと結果の構造体はintとlongだけでできたblittable型で、変換せずにポインターで渡せる。boolはblittableではないので、合否もintにした。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
blittable型はStructLayoutで構成できます。記事の2つの構造体はintとlongだけでできたblittable型で、LayoutKind.Sequentialを指定してCの宣言と同じ順にフィールドを並べた。C#のsizeofとAdaのinspect_result_sizeで大きさを比べてから検査を始める。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
P/Invokeは呼び出し規約(calling convention)を前提とします。AdaはConvention => Cで関数を公開しているので、C#の側はCallConvCdeclを指定する。x86のWindowsではP/Invokeの既定がStdcallで、x64では呼び出し規約が1つなので指定は結果を変えない。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
P/InvokeはDLL(ダイナミックリンクライブラリ)を利用します。LibraryImportにlibinspectと書くと、.NETはWindowsではlibinspectとlibinspect.dllを、Linuxではlibinspect.soなどを探すので、gprbuildが作るlibinspect.dllとlibinspect.soのどちらにも届く。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
SPARKはGNATproveを利用します。判定の関数を置いたInspect_CoreはSPARKのパッケージとしてGNATproveで証明し、ポインターを配列として扱う境界の関数はSPARKの外に置いてテストとレビューで確かめる。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
GNATproveはSPARK_Modeで構成できます。判定の関数のパッケージにはSPARK_Modeを付けて証明の対象にし、境界の関数のパッケージには付けていない。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
契約による設計(Pre/Post)はGNATproveで確認できます。判定の関数の事前条件(行が1つ以上で、幅が列の数以下)と事後条件をGNATproveで確かめる。事前条件は、境界の関数が寸法を確かめてから呼ぶことで満たす。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
整数オーバーフローはGNATproveで確認できます。欠陥の画素は1行の数をNatural、全体の数を64ビットの整数で数え、どちらもあふれないことをGNATproveで証明した。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
AdaとC/C++の相互運用(Annex B)は未処理例外の原因になることがあります。処理しなかったAdaの例外をC#まで届かせると、プロセスが終了しうる。記事の境界の関数は、パラメーターの範囲外をifで確かめて4を返し、想定していない例外はすべて99のエラーコードに変えて返し、例外を外へ出さない。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
スタンドアロンライブラリ(Stand-alone Library)はGPRbuildで構成できます。GPRbuildのライブラリプロジェクトでLibrary_Kindを"dynamic"にし、Library_InterfaceにInspect_APIを指定して、スタンドアロンライブラリを作る。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
スタンドアロンライブラリ(Stand-alone Library)はエラボレーション(elaboration)を自動化します。Library_Auto_Initを"true"にすると、スタンドアロンライブラリは自動で初期化される。記事の例では、初期化で1にする変数を返すinspect_elaboratedが、LinuxでもWindowsのランナーでも1を返した。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
Adaのタスク(並行処理)はスタンドアロンライブラリ(Stand-alone Library)と両立しません。Windowsではスタンドアロンライブラリにライブラリのレベルのタスクを置けない。記事はこの制約を既存の記事に任せ、例のパッケージにはタスクがないことを書く。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
スタンドアロンライブラリ(Stand-alone Library)はDLL(ダイナミックリンクライブラリ)を利用します。WindowsのランナーでAlireのGNATが作ったスタンドアロンライブラリはlibinspect.dllになり、GNATのランタイムのDLLに依存した。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
DLL(ダイナミックリンクライブラリ)はDLLの検索順序を前提とします。libinspect.dllとGNATのランタイムのDLLは、Windowsが探すフォルダー(記事ではアプリのフォルダー)に置く。記事のWindowsでのテストでは、ランタイムのDLLを除くとDllNotFoundExceptionでプロセスが終了した。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典出典
WPFはUIスレッドのコンテキストを前提とします。WPFのUI要素は作ったスレッドからしか触れないので、記事の例では検査をTask.Runで別のスレッドで行い、結果の表示はawaitのあとUIスレッドに戻ってから行う。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典

主要概念の定義

AdaとC/C++の相互運用(Annex B): Ada参照マニュアルの附属書Bで標準化された、C・Fortranなど他言語とのインターフェース機構。ImportやExportで双方向の呼び出しができる。
P/Invoke: C#などの.NETコードからアンマネージドなC関数群を呼び出すための、.NETの標準的な相互運用機構。
LibraryImport: .NET 7で追加された、partialメソッドに対しコンパイル時にP/Invokeのマーシャリングコードを生成するソースジェネレーター。
blittable型: マネージドコードとアンマネージドコードの間でメモリ表現が同一で、変換なしにそのまま受け渡せる型。UnmanagedCallersOnlyを付けたメソッドのシグネチャに使える型はこれに限られる。
SPARK: プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。
GNATprove: AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。
契約による設計(Pre/Post): サブプログラムの入口での前提条件(Pre)と、出口で保証する性質(Post)を宣言的に記述する、Ada 2012の契約機構である。
整数オーバーフロー: 整数の演算結果が、その型で表せる範囲を超えること。言語と設定によって、例外・パニック・折り返しのいずれかになる。Adaでは、値が型の基本範囲に収まるかを確かめるOverflow_Checkに失敗すると、実行時にConstraint_Errorが送出される。
スタンドアロンライブラリ(Stand-alone Library): GPRbuildのライブラリプロジェクトでLibrary_Interfaceに外部へ見せるユニットを指定して作るAdaのライブラリ。初期化と終了処理の手続きを持ち、Ada以外の言語のプログラムから使える。
Adaのタスク(並行処理): スレッドをOSのAPIやライブラリに頼らず、言語仕様に組み込む形で提供するAdaの並行実行単位。
DLL(ダイナミックリンクライブラリ): 実行時に読み込まれ、関数やデータを他のモジュールと共有できるWindowsのバイナリモジュール。
WPF: XAMLでUIを宣言的に記述する、Windows専用のデスクトップUIフレームワーク。ベクターベースの描画とデータバインディングを特徴とする。

機械可読データ

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

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

作成: 合同会社小村ソフト
ライセンス: CC BY 4.0 ── 出典(合同会社小村ソフト)とライセンスへのリンクを明示し、改変した場合はその旨を示すことを条件に、再配布・改変を含めて再利用できます
最終確認日: 2026-11-10 ── 収録する関係のうち、最後に出典と照合した日

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