知識マップ: ピクセルとミリメートルを型で分ける ── Adaで寸法検査の単位の取り違えを防ぐ

記事「ピクセルとミリメートルを型で分ける ── Adaで寸法検査の単位の取り違えを防ぐ」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

AdaではLong_Floatから派生した型どうしは別の型になり、ピクセルの長さをミリメートルの変数にそのまま入れるとコンパイルエラーになる。ただし派生型は親の型の基本演算を受け継ぐので、ピクセルの長さどうしの掛け算がピクセルの長さを返す。型を宣言したパッケージの仕様部で意味のない演算子をis abstractと宣言し直すと呼べなくなり、意味のある演算子だけを定義できる。座標・長さ・校正係数の型を総称パッケージにまとめてx用とy用にインスタンス化すると、軸ごとに別の型になり、x方向の係数をy方向の長さに掛ける式がコンパイルエラーになる。公差の判定は浮動小数点数のまま比べると上限ちょうどの値が不合格になることがあり、10進固定小数点型に丸めてから比べる。GNATは独自のアスペクトで次元解析を行えるが、座標と長さは区別できない。固定小数点型で書いた換算の範囲検査が失敗しないことは、GNATproveで証明できる。

flowchart LR
    accTitle: ピクセルとミリメートルを型で分ける記事の知識マップ
    accDescr: Adaの強い型付けが派生型で単位の混用を防ぎ、派生型が受け継いだ意味のない演算子を抽象サブプログラムで消すこと、総称パッケージで軸ごとの型を作ること、固定小数点型の範囲検査をGNATproveで証明すること、GNATが独自の次元解析を実装することを示す図。
    ada_strong_typing["Adaの強い型付け"]
    ada_derived_type["派生型(derived type)"]
    gnat["GNAT"]
    ada["Ada(プログラミング言語)"]
    ada_abstract_subprogram["抽象サブプログラム(abstract subprogram)"]
    ada_generic_package["総称パッケージ(Generic Package)"]
    ada_fixed_point_type["固定小数点型(fixed point type)"]
    ada_range_constraint["範囲制約(range constraint)"]
    gnatprove["GNATprove"]
    spark["SPARK"]
    gnat_dimensionality_checking["GNATの次元解析(Dimension_System)"]
    gnat -->|"実装を担う"| ada
    ada -->|"実装を担う"| ada_strong_typing
    ada_strong_typing -->|"利用する"| ada_derived_type
    ada_strong_typing -.->|"利用する"| ada_abstract_subprogram
    ada_generic_package -.->|"利用する"| ada_derived_type
    ada -->|"実装を担う"| ada_fixed_point_type
    ada_fixed_point_type -->|"利用する"| ada_range_constraint
    ada_range_constraint -.->|"で確認できる"| gnatprove
    spark -->|"利用する"| gnatprove
    gnat -->|"実装を担う"| gnat_dimensionality_checking

概念間の関係(全10件)

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

• GNATはAda(プログラミング言語)の実装を担います。GNATはAda言語のコンパイラとしての実装を担う処理系で、記事の例はGNAT 13.3.0とGNAT 16.1.0でコンパイルして実行した。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• Ada(プログラミング言語)はAdaの強い型付けの実装を担います。記事の例では、Long_Floatから派生したピクセルの長さ、座標、ミリメートル、校正係数を別の型にし、型変換を書かない限り混ぜられないようにして、単位の合わない式をコンパイル時に見つけた。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• Adaの強い型付けは派生型(derived type)を利用します。Long_Floatから派生したPx_LengthとMm_Lengthは別の型になり、型変換なしに混ぜて使えない。記事の例では、ピクセルの長さをミリメートルの変数に入れる式がexpected type、found typeのエラーになった。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• Adaの強い型付けは抽象サブプログラム(abstract subprogram)を利用します。派生型は親の型の基本演算を受け継ぐので、ピクセルの長さどうしの掛け算やべき乗がピクセルの長さを返す。型を宣言したパッケージの仕様部で意味のない演算子をis abstractと宣言し直すと、その演算子は呼べなくなり、単位の合わない式がコンパイルエラーになる。記事の例では、GNATがcannot call abstract operationと報告した。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典 出典
• 総称パッケージ(Generic Package)は派生型(derived type)を利用します。記事のVision_Units.Axisは、座標・長さ・2つの向きの校正係数を派生型として宣言する総称パッケージである。x用とy用に2回インスタンス化すると、インスタンスごとに別の型になり、y方向の長さにx方向の係数を掛ける式がコンパイルエラーになった。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
• Ada(プログラミング言語)は固定小数点型(fixed point type)の実装を担います。固定小数点型はAdaの言語仕様が定める実数の型で、普通の固定小数点型と10進固定小数点型がある。10進固定小数点型はsmallがdeltaと同じ10のべき乗なので、0.001 mm刻みの図面の値を誤差なく表せる。記事の例では、Long_Floatのまま比べると上限ちょうどの5.10 mmが不合格になり、'Roundで丸めてから比べると合格になった。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典 出典
• 固定小数点型(fixed point type)は範囲制約(range constraint)を利用します。記事のScaled_Lengthでは、固定小数点型の宣言にrangeを書いて値の範囲を決めている。固定小数点型どうしの掛け算の結果をMmに型変換するときに、範囲検査が行われる。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典 出典
• 範囲制約(range constraint)はGNATproveで確認できます。長さの上限16384 pxと係数の上限1.0 mm/pxから、換算の結果がMmの範囲に収まることをGNATproveで証明した。長さの上限を1000000 pxに広げた版では証明できず、通常のビルドでは実行時にConstraint_Errorになった。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
• SPARKはGNATproveを利用します。SPARK_Modeを付けたパッケージScaled_Lengthを、GNATproveで証明した。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• GNATはGNATの次元解析(Dimension_System)の実装を担います。Dimension_SystemとDimensionはGNATの処理系定義のアスペクトで、Adaの規格にはない。記事の例ではmmとx・yのピクセルを基本の次元にし、px×px、係数の掛け忘れ、xとyの取り違え、係数の向きの逆が次元の不一致として報告された。座標と長さはどちらも同じ次元なので区別できない。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典 出典

主要概念の定義

Adaの強い型付け

構造が同じでも別名で宣言した型を別の型として扱い、暗黙の混用をコンパイルエラーにするAdaの型システムの性質。

派生型(derived type)

type T is new 親の型 の形で宣言する、親の型と同じ値の集合と基本演算を受け継いだ別の型。親の型や、同じ親から派生したほかの型と、型変換なしに混ぜて使えない。

GNAT

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

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

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

総称パッケージ(Generic Package)

複数の操作と内部状態をまとめて再利用するための、generic宣言に続けて書くパッケージの雛形。インスタンスごとに内部状態は独立する。

固定小数点型(fixed point type)

誤差の上限をdeltaで指定し、値を刻み(small)の整数倍で表すAdaの実数型。普通の固定小数点型と、smallがdeltaに等しく10のべき乗になる10進固定小数点型がある。

範囲制約(range constraint)

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

SPARK

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

機械可読データ

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

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

作成

合同会社小村ソフト

ライセンス

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

最終確認日

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

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