@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-pixel-millimeter-types/#article>
    schema:about <https://comcomponent.com/knowledge/ada-strong-typing/>, <https://comcomponent.com/knowledge/ada-derived-type/> ;
    schema:mentions <https://comcomponent.com/knowledge/ada/>, <https://comcomponent.com/knowledge/gnat/>, <https://comcomponent.com/knowledge/ada-abstract-subprogram/>, <https://comcomponent.com/knowledge/ada-generic-package/>, <https://comcomponent.com/knowledge/ada-generic-instantiation/>, <https://comcomponent.com/knowledge/ada-fixed-point-type/>, <https://comcomponent.com/knowledge/ada-range-constraint/>, <https://comcomponent.com/knowledge/gnat-dimensionality-checking/>, <https://comcomponent.com/knowledge/spark/>, <https://comcomponent.com/knowledge/gnatprove/> .

<https://comcomponent.com/knowledge/ada-strong-typing/> a skos:Concept ;
    skos:prefLabel "Adaの強い型付け"@ja ;
    skos:definition "構造が同じでも別名で宣言した型を別の型として扱い、暗黙の混用をコンパイルエラーにするAdaの型システムの性質。"@ja ;
    skos:altLabel "strong typing" ;
    ks:uses <https://comcomponent.com/knowledge/ada-derived-type/> .

<https://comcomponent.com/knowledge/ada-derived-type/> a skos:Concept ;
    skos:prefLabel "派生型(derived type)"@ja ;
    skos:definition "type T is new 親の型 の形で宣言する、親の型と同じ値の集合と基本演算を受け継いだ別の型。親の型や、同じ親から派生したほかの型と、型変換なしに混ぜて使えない。"@ja ;
    skos:altLabel "derived type" ;
    skos:altLabel "type ... is new" .

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

<https://comcomponent.com/knowledge/ada/> a skos:Concept ;
    skos:prefLabel "Ada(プログラミング言語)"@ja ;
    skos:definition "1970年代後半にアメリカ国防総省の主導で標準化された、強い型付けと高信頼性を重視する汎用プログラミング言語。最新標準はAda 2022。"@ja ;
    skos:altLabel "Ada言語"@ja ;
    skos:altLabel "Ada 2022" ;
    ks:implements <https://comcomponent.com/knowledge/ada-strong-typing/> ;
    ks:implements <https://comcomponent.com/knowledge/ada-fixed-point-type/> .

<https://comcomponent.com/knowledge/ada-abstract-subprogram/> a skos:Concept ;
    skos:prefLabel "抽象サブプログラム(abstract subprogram)"@ja ;
    skos:definition "is abstract を付けて宣言する、本体を持たないAdaのサブプログラム。ディスパッチしない形で呼ぶとコンパイルエラーになる。"@ja ;
    skos:altLabel "abstract subprogram" ;
    skos:altLabel "is abstract" .

<https://comcomponent.com/knowledge/ada-generic-package/> a skos:Concept ;
    skos:prefLabel "総称パッケージ(Generic Package)"@ja ;
    skos:definition "複数の操作と内部状態をまとめて再利用するための、generic宣言に続けて書くパッケージの雛形。インスタンスごとに内部状態は独立する。"@ja ;
    skos:altLabel "generic package" ;
    skos:altLabel "総称パッケージ"@ja ;
    skos:broader <https://comcomponent.com/knowledge/ada-generics/> .

<https://comcomponent.com/knowledge/ada-fixed-point-type/> a skos:Concept ;
    skos:prefLabel "固定小数点型(fixed point type)"@ja ;
    skos:definition "誤差の上限をdeltaで指定し、値を刻み(small)の整数倍で表すAdaの実数型。普通の固定小数点型と、smallがdeltaに等しく10のべき乗になる10進固定小数点型がある。"@ja ;
    skos:altLabel "fixed point type" ;
    skos:altLabel "10進固定小数点型"@ja ;
    skos:altLabel "decimal fixed point type" ;
    ks:uses <https://comcomponent.com/knowledge/ada-range-constraint/> .

<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" .

<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/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/gnat-dimensionality-checking/> a skos:Concept ;
    skos:prefLabel "GNATの次元解析(Dimension_System)"@ja ;
    skos:definition "GNAT独自のアスペクトDimension_SystemとDimensionで浮動小数点型とそのsubtypeに次元を持たせ、式の次元が合わないことをコンパイル時に検出する仕組み。Adaの規格にはない。"@ja ;
    skos:altLabel "Dimensionality Analysis" ;
    skos:altLabel "Dimension_System" ;
    skos:altLabel "Dimension アスペクト"@ja .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/gnat/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/ada/> ;
    schema:description "GNATはAda言語のコンパイラとしての実装を担う処理系で、記事の例はGNAT 13.3.0とGNAT 16.1.0でコンパイルして実行した。"@ja ;
    ks:evidence <https://gcc.gnu.org/onlinedocs/gnat_ugn/> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/ada-strong-typing/> ;
    schema:description "記事の例では、Long_Floatから派生したピクセルの長さ、座標、ミリメートル、校正係数を別の型にし、型変換を書かない限り混ぜられないようにして、単位の合わない式をコンパイル時に見つけた。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-4.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-strong-typing/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/ada-derived-type/> ;
    schema:description "Long_Floatから派生したPx_LengthとMm_Lengthは別の型になり、型変換なしに混ぜて使えない。記事の例では、ピクセルの長さをミリメートルの変数に入れる式がexpected type、found typeのエラーになった。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-4.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-strong-typing/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/ada-abstract-subprogram/> ;
    schema:description "派生型は親の型の基本演算を受け継ぐので、ピクセルの長さどうしの掛け算やべき乗がピクセルの長さを返す。型を宣言したパッケージの仕様部で意味のない演算子をis abstractと宣言し直すと、その演算子は呼べなくなり、単位の合わない式がコンパイルエラーになる。記事の例では、GNATがcannot call abstract operationと報告した。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-4.html>, <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-9-3.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-generic-package/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/ada-derived-type/> ;
    schema:description "記事のVision_Units.Axisは、座標・長さ・2つの向きの校正係数を派生型として宣言する総称パッケージである。x用とy用に2回インスタンス化すると、インスタンスごとに別の型になり、y方向の長さにx方向の係数を掛ける式がコンパイルエラーになった。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-12-3.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/ada-fixed-point-type/> ;
    schema:description "固定小数点型はAdaの言語仕様が定める実数の型で、普通の固定小数点型と10進固定小数点型がある。10進固定小数点型はsmallがdeltaと同じ10のべき乗なので、0.001 mm刻みの図面の値を誤差なく表せる。記事の例では、Long_Floatのまま比べると上限ちょうどの5.10 mmが不合格になり、'Roundで丸めてから比べると合格になった。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-5-9.html>, <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-4-6.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-fixed-point-type/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/ada-range-constraint/> ;
    schema:description "記事のScaled_Lengthでは、固定小数点型の宣言にrangeを書いて値の範囲を決めている。固定小数点型どうしの掛け算の結果をMmに型変換するときに、範囲検査が行われる。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-5-9.html>, <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-4-5-5.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-range-constraint/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "長さの上限16384 pxと係数の上限1.0 mm/pxから、換算の結果がMmの範囲に収まることをGNATproveで証明した。長さの上限を1000000 pxに広げた版では証明できず、通常のビルドでは実行時にConstraint_Errorになった。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_run_gnatprove.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "SPARK_Modeを付けたパッケージScaled_Lengthを、GNATproveで証明した。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_run_gnatprove.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/gnat/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/gnat-dimensionality-checking/> ;
    schema:description "Dimension_SystemとDimensionはGNATの処理系定義のアスペクトで、Adaの規格にはない。記事の例ではmmとx・yのピクセルを基本の次元にし、px×px、係数の掛け忘れ、xとyの取り違え、係数の向きの逆が次元の不一致として報告された。座標と長さはどちらも同じ次元なので区別できない。"@ja ;
    ks:evidence <https://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ugn/gnat_and_program_execution.html>, <https://docs.adacore.com/gnat_rm-docs/html/gnat_rm/gnat_rm/implementation_defined_aspects.html> ;
    ks:verifiedAt "2026-11-10" ;
    ks:certainty "established" .