画像で部品の寸法を測るプログラムでは、ピクセル（px）とミリメートル（mm）の値が同じ計算の中を流れます。どちらも double のような浮動小数点数で持つことが多く、校正係数を掛け忘れても、x 方向の係数を y 方向の長さに掛けても、コンパイラーはエラーも警告も出しません。間違いは合否の判定がずれて初めて見つかります。
Ada では画像上の座標、ピクセルの長さ、ミリメートル、校正係数（mm/px）をそれぞれ別の型にして、意味のある演算だけを残せます。この記事では寸法検査で起きやすい単位の取り違えを挙げ、それぞれがコンパイルエラーになる型の作り方を、実際に GNAT で出したエラーとともに説明します。後半では公差の判定に10進固定小数点型を使う理由と GNAT 独自の次元系を扱います。最後に、換算の結果が型の範囲からはみ出さないことを SPARK で証明します。
コンパイルと実行は2026年11月10日に、手元の Ubuntu 24.04 の GNAT 13.3.0 で行い、記事に載せたエラーメッセージと出力はその結果です。
GNATprove による証明は GitHub Actions の Ubuntu 24.04 のランナーで、Alire 2.1.1 が用意した GNAT 16.1.0 と GNATprove FSF 16.1.0 を使って行いました。同じランナーでほかの例もビルドして実行し、エラーメッセージと出力が手元と同じになることを確かめています。
派生型の基本は Ada言語の魅力 と Ada と Rust の安全性の考え方の違い で説明しているので、ここでは寸法検査に必要なところから始めます。
寸法検査で単位を取り違える場所
エッジの検出から合否の判定までを追うと、値は次の順に単位を変えます。エッジの検出は画像上の座標（px）を返し、2つの座標の差が長さ（px）になります。長さに校正係数（mm/px）を掛けるとミリメートルの長さになり、最後に図面の公差と比べます。
flowchart TB
accTitle: 寸法検査で値の単位が変わる順序
accDescr: エッジの検出が返す座標の差を取って長さにし、校正係数を掛けてミリメートルにし、図面の公差と比べて合否を決める流れを示す。
A["画像"] -->|"エッジを検出する"| B["エッジの座標（px）"]
B -->|"2点の差を取る"| C["長さ（px）"]
C -->|"校正係数（mm/px）を掛ける"| D["長さ（mm）"]
D -->|"図面の公差と比べる"| E["合否"]
図1: エッジの座標から合否までの間に、値は座標、ピクセルの長さ、ミリメートルの長さの順に変わる。
この流れの中で、次の取り違えが起きます。値がすべて浮動小数点数なら、どれもコンパイルは通ります。
- ピクセルの長さどうしを掛け、面積（px²）を長さとして扱う。
- 校正係数を掛け忘れ、ピクセルの長さをミリメートルとして判定に回す。
- 差を取り忘れ、エッジの座標をそのまま長さとして換算する。
- x 方向の校正係数を y 方向の長さに掛ける（画素の縦横比や光学系によって、x と y で係数が違うことがある）。
- 校正係数の向きを逆にする（mm/px の係数と px/mm の係数を取り違える）。
flowchart TB
accTitle: 取り違えが起きる段階
accDescr: 座標の段階では座標を長さとして換算する誤り、長さの段階では掛け算で面積を長さにする誤りと係数の掛け忘れ、係数を掛ける段階ではx方向とy方向の取り違えと係数の向きの逆が起きることを示す。
B["エッジの座標（px）"] --> C["長さ（px）"]
C --> D["長さ（mm）"]
B -.-> M1["座標を長さとして換算する"]
C -.-> M2["px × px を長さとして扱う"]
C -.-> M3["校正係数を掛け忘れる"]
D -.-> M4["x と y の係数を取り違える"]
D -.-> M5["mm/px と px/mm を逆にする"]
図2: 5つの取り違えは座標、ピクセルの長さ、ミリメートルへの換算の3つの段階で起きる。
図の実線は常に成り立つ関係、破線は条件付きの関係です(成立条件は詳細ページの各関係の説明に記載)。関係すべての一覧(全10件、根拠・確度つき)と主要概念の定義は知識マップ詳細ページにまとめています。データ: JSON-LD / Turtle
派生型にしただけでは px × px が通る
Ada で type Px_Length is new Long_Float; と書くと、Long_Float から派生した別の型ができます。別の型なので、Px_Length の値を Mm_Length の変数にそのまま入れるとコンパイルエラーになります。ただし、派生型は親の型の基本演算を受け継ぎます1。Long_Float の掛け算は Long_Float を返すので、Px_Length の掛け算も Px_Length を返します。
with Ada.Text_IO; use Ada.Text_IO;
procedure Naive_Check is
type Px_Length is new Long_Float;
type Mm_Length is new Long_Float;
Width : constant Px_Length := 510.0;
Area : constant Px_Length := Width * Width; -- px × px が px になる
Scale : constant Px_Length := 0.01; -- mm/px のつもりの値
Wrong : constant Mm_Length := Mm_Length (Width * Scale);
begin
Put_Line (Px_Length'Image (Area));
Put_Line (Mm_Length'Image (Wrong));
end Naive_Check;
このプログラムは警告なしでコンパイルでき、次のように出力しました。
2.60100000000000E+05
5.10000000000000E+00
面積を長さの型に入れる式が通っています。校正係数の行にも問題があります。係数を Px_Length で宣言したのは、別の型にすると Width * Scale が書けなくなるからです。型を分けたまま計算するには Mm_Length (Long_Float (Width) * Long_Float (Scale)) のような型変換が要ります。型変換を書いた箇所では型の検査が効かないので、変換を重ねるほど型を分けた意味が薄れます。
flowchart TB
accTitle: 派生型が受け継ぐ演算子
accDescr: Long_Floatから派生したPx_Lengthが四則演算をそのまま受け継ぎ、Px_Lengthどうしの掛け算がPx_Lengthを返すこと、係数を別の型にすると型変換が必要になることを示す。
F["Long_Float"] -->|"type … is new"| P["Px_Length"]
P --> O["四則演算をそのまま受け継ぐ"]
O --> A["px × px が Px_Length を返す"]
P -.-> S["係数を別の型にすると掛け算が書けない"]
S -.-> C["型変換を書くと検査が効かない"]
図3: 派生型は別の型になるが、親の型の演算子も受け継ぐので、意味のない掛け算が通る。
意味のない演算子を abstract で消す
受け継いだ演算子は型を宣言したパッケージの仕様部で is abstract を付けて宣言し直すと、呼べなくなります。本体を持たない抽象サブプログラムは、ディスパッチしない形で呼ぶとコンパイルエラーになるからです2。ディスパッチしない抽象サブプログラムは名前解決の候補にもなりません3。そのうえで、意味のある演算子だけを自分で定義します。Ada では演算子の名前の関数を宣言でき、引数と戻り値の型の組み合わせごとに別の関数として扱われます4。
ミリメートルの型は次のように書きました。
package Vision_Units is
type Millimeters is new Long_Float;
-- mm × mm、mm ÷ mm、mm のべき乗を mm として返す演算は意味がないので消す
function "*" (Left, Right : Millimeters) return Millimeters is abstract;
function "/" (Left, Right : Millimeters) return Millimeters is abstract;
function "**" (Left : Millimeters; Right : Integer) return Millimeters is abstract;
-- 何倍するか、何分の一にするかは無次元の数で書く
function "*" (Left : Long_Float; Right : Millimeters) return Millimeters;
function "/" (Left : Millimeters; Right : Long_Float) return Millimeters;
end Vision_Units;
足し算、引き算、比較は残しています。ミリメートルどうしを足した結果はミリメートルなので、受け継いだ演算子のままで意味が合います。掛け算と割り算は、ミリメートルどうしで結果もミリメートルになる演算を消し、無次元の Long_Float を相手にする演算だけを定義しました。べき乗の ** も Long_Float から受け継ぎますが、mm² を mm として返すので消しています。
flowchart TB
accTitle: Millimetersに残す演算子と消す演算子
accDescr: Millimetersの足し算・引き算・比較は受け継いだまま残し、Millimeters同士の掛け算・割り算とべき乗はabstractで消し、Long_Floatとの掛け算と割り算を新しく定義することを示す。
M["Millimeters"] --> K["残す：足し算・引き算・比較"]
M --> X["abstract で消す：mm × mm、mm ÷ mm、mm ** n"]
M --> N["定義する：数 × mm、mm ÷ 数"]
図4: 結果の単位が合う演算子は残し、合わない演算子は abstract で消し、必要な組み合わせだけを定義する。
ピクセルの型は軸ごとに総称パッケージで作る
ピクセルの側には座標、長さ、2つの向きの校正係数の4つの型が要ります。これを x 方向と y 方向で別々に用意するため、型と演算子を総称パッケージ（generic package）にまとめ、x 用と y 用に2回インスタンス化します。インスタンスは総称パッケージの写しで、中で宣言した型はインスタンスごとに別の型になります5。
generic
package Vision_Units.Axis is
type Position is new Long_Float; -- 画像上の座標（px）
type Length is new Long_Float; -- 2点の間の長さ（px）
type Mm_Per_Px is new Long_Float; -- 校正係数（mm/px）
type Px_Per_Mm is new Long_Float; -- その逆数（px/mm）
-- 座標どうしの足し算・掛け算・割り算は意味がないので消す
function "+" (Left, Right : Position) return Position is abstract;
function "*" (Left, Right : Position) return Position is abstract;
function "/" (Left, Right : Position) return Position is abstract;
-- 座標を返す引き算とべき乗も座標には意味がない
function "-" (Left, Right : Position) return Position is abstract;
function "**" (Left : Position; Right : Integer) return Position is abstract;
-- px × px や px のべき乗を px として返す演算も消す
function "*" (Left, Right : Length) return Length is abstract;
function "/" (Left, Right : Length) return Length is abstract;
function "**" (Left : Length; Right : Integer) return Length is abstract;
-- 校正係数どうしの掛け算・割り算・べき乗も消す
function "*" (Left, Right : Mm_Per_Px) return Mm_Per_Px is abstract;
function "/" (Left, Right : Mm_Per_Px) return Mm_Per_Px is abstract;
function "**" (Left : Mm_Per_Px; Right : Integer) return Mm_Per_Px is abstract;
function "*" (Left, Right : Px_Per_Mm) return Px_Per_Mm is abstract;
function "/" (Left, Right : Px_Per_Mm) return Px_Per_Mm is abstract;
function "**" (Left : Px_Per_Mm; Right : Integer) return Px_Per_Mm is abstract;
-- 座標と長さの関係
function "-" (Left, Right : Position) return Length;
function "+" (Left : Position; Right : Length) return Position;
function "-" (Left : Position; Right : Length) return Position;
-- 長さを何倍するか、何分の一にするか
function "*" (Left : Long_Float; Right : Length) return Length;
function "/" (Left : Length; Right : Long_Float) return Length;
-- 単位の変換は、この2つの向きだけ
function "*" (Left : Length; Right : Mm_Per_Px) return Millimeters;
function "*" (Left : Millimeters; Right : Px_Per_Mm) return Length;
-- 既知の寸法を写した画像から校正係数を求める
function "/" (Left : Millimeters; Right : Length) return Mm_Per_Px;
-- 係数の向きを変える
function Invert (Scale : Mm_Per_Px) return Px_Per_Mm;
end Vision_Units.Axis;
with Vision_Units.Axis;
package X_Axis is new Vision_Units.Axis;
with Vision_Units.Axis;
package Y_Axis is new Vision_Units.Axis;
Vision_Units.Axis は Vision_Units の子の総称パッケージなので、親で宣言した Millimeters をそのまま使えます。本体は引数を Long_Float に変換して計算し、戻り値の型に変換するだけです。型変換はこの本体の中に閉じ込め、利用する側には書かせません。
flowchart TB
accTitle: 総称パッケージのインスタンスごとに別の型ができる
accDescr: 総称パッケージVision_Units.AxisをX_AxisとY_Axisの2つにインスタンス化すると、X_Axis.LengthとY_Axis.Lengthのような別々の型ができ、Millimetersは親パッケージの1つの型を共有することを示す。
G["Vision_Units.Axis（総称パッケージ）"] -->|"new"| X["X_Axis"]
G -->|"new"| Y["Y_Axis"]
X --> XL["X_Axis.Length など4つの型"]
Y --> YL["Y_Axis.Length など4つの型"]
P["Vision_Units.Millimeters"] -.->|"x と y で共有する"| XL
P -.-> YL
図5: インスタンスごとに座標・長さ・係数の型が別にでき、ミリメートルの型だけを x と y で共有する。
座標と長さの間には次の3つの関係だけを定義しました。座標から座標を引くと長さになり、座標に長さを足したり引いたりすると座標になります。受け継いだ演算子のうち、座標どうしの足し算・掛け算・割り算、座標を返す引き算、べき乗は消しました。
符号を反転する単項の - と abs は座標にも残しています。消すと、-5.0 のような負の座標をリテラルで書けなくなるからです。GNAT 13.3.0 で試すと、P : constant Position := -5.0; が cannot call abstract operation "-" になりました。長さ、ミリメートル、校正係数どうしの足し算と引き算は、結果の単位が変わらないので残しています。
flowchart TB
accTitle: 座標と長さの間に定義した演算
accDescr: 座標から座標を引くと長さ、座標に長さを足し引きすると座標、長さに校正係数を掛けるとミリメートルになり、座標どうしの足し算と長さどうしの掛け算は消したことを示す。
P1["座標 − 座標"] --> L["長さ"]
P2["座標 ± 長さ"] --> P["座標"]
L2["長さ × mm/px"] --> M["ミリメートル"]
M2["ミリメートル × px/mm"] --> L3["長さ"]
N1["座標 + 座標"] -.-> E["abstract で消した"]
N2["長さ × 長さ"] -.-> E
図6: 座標・長さ・ミリメートルの間で、結果の単位が決まる演算だけを残した。
取り違えごとに GNAT が出すエラー
図2の5つの取り違えに、中点の計算とべき乗・座標を返す引き算の2つを加え、それぞれ小さなプログラムにしてコンパイルしました。どれも GNAT 13.3.0 でコンパイルエラーになりました。GitHub Actions の GNAT 16.1.0 でも、メッセージは列の番号まで同じでした。
ピクセルの長さどうしを掛ける
with X_Axis; use X_Axis;
procedure Err_Px_Times_Px is
Width : constant Length := 510.0;
Area : constant Length := Width * Width;
begin
null;
end Err_Px_Times_Px;
err_px_times_px.adb:5:37: error: cannot call abstract operation "*" declared at vision_units-axis.ads:19, instance at x_axis.ads:2
abstract で消した演算子を呼んだので、cannot call abstract operation と報告されました。面積が必要なら、面積の型と Length × Length → 面積 の演算子を別に定義します。
校正係数を掛け忘れる
with Vision_Units; use Vision_Units;
with X_Axis; use X_Axis;
procedure Err_Forgot_Scale is
Width_Px : constant Length := 510.0;
Width_Mm : constant Millimeters := Width_Px;
begin
null;
end Err_Forgot_Scale;
err_forgot_scale.adb:6:39: error: expected type "Millimeters" defined at vision_units.ads:3
err_forgot_scale.adb:6:39: error: found type "Length" defined at vision_units-axis.ads:5, instance at x_axis.ads:2
座標をそのまま長さとして換算する
with Vision_Units; use Vision_Units;
with X_Axis; use X_Axis;
procedure Err_Position_As_Length is
Scale : constant Mm_Per_Px := 0.020;
Right_Edge : constant Position := 630.75;
Width_Mm : constant Millimeters := Right_Edge * Scale;
begin
null;
end Err_Position_As_Length;
err_position_as_length.adb:7:52: error: invalid operand types for operator "*"
err_position_as_length.adb:7:52: error: left operand has type "Position" defined at vision_units-axis.ads:4, instance at x_axis.ads:2
err_position_as_length.adb:7:52: error: right operand has type "Mm_Per_Px" defined at vision_units-axis.ads:6, instance at x_axis.ads:2
校正係数を掛けられるのは長さだけなので、座標に掛ける式は書けません。
座標どうしを足して中点を求める
座標どうしの足し算を消したので、中点を (左 + 右) / 2.0 と書く式もコンパイルエラーになります。この式は数値としては正しく求まりますが、座標どうしを足せるようにすると、座標と長さを同じ値として扱う式も書けてしまいます。この記事の型では中点を「左端 + 長さの半分」と書きます。
with X_Axis; use X_Axis;
procedure Err_Center is
Left_Edge : constant Position := 120.25;
Right_Edge : constant Position := 630.75;
Center : constant Position := (Left_Edge + Right_Edge) / 2.0;
begin
null;
end Err_Center;
err_center.adb:6:49: error: cannot call abstract operation "+" declared at vision_units-axis.ads:10, instance at x_axis.ads:2
y 方向の長さに x 方向の係数を掛ける
with Vision_Units; use Vision_Units;
with X_Axis;
with Y_Axis;
procedure Err_Y_With_X_Scale is
Scale_X : constant X_Axis.Mm_Per_Px := 0.020;
Height : constant Y_Axis.Length := 300.0;
Height_Mm : constant Millimeters := Height * Scale_X;
begin
null;
end Err_Y_With_X_Scale;
err_y_with_x_scale.adb:8:47: error: invalid operand types for operator "*"
err_y_with_x_scale.adb:8:47: error: left operand has type "Length" defined at vision_units-axis.ads:5, instance at y_axis.ads:2
err_y_with_x_scale.adb:8:47: error: right operand has type "Mm_Per_Px" defined at vision_units-axis.ads:6, instance at x_axis.ads:2
メッセージの instance at y_axis.ads:2 と instance at x_axis.ads:2 で、どちらのインスタンスの型かが分かります。
mm/px と px/mm を取り違える
with Vision_Units; use Vision_Units;
with X_Axis; use X_Axis;
procedure Err_Inverse_Scale is
Scale : constant Px_Per_Mm := 50.0;
Width_Px : constant Length := 510.0;
Width_Mm : constant Millimeters := Width_Px * Scale;
begin
null;
end Err_Inverse_Scale;
err_inverse_scale.adb:7:48: error: invalid operand types for operator "*"
err_inverse_scale.adb:7:48: error: left operand has type "Length" defined at vision_units-axis.ads:5, instance at x_axis.ads:2
err_inverse_scale.adb:7:48: error: right operand has type "Px_Per_Mm" defined at vision_units-axis.ads:7, instance at x_axis.ads:2
Length × Px_Per_Mm の演算子は定義していないので、この式は書けません。px/mm の係数を使えるのは、ミリメートルをピクセルに直す Millimeters × Px_Per_Mm だけです。
べき乗と、座標を返す引き算
最初に書いた型では +、*、/ だけを消していたので、Long_Float から受け継いだほかの演算子が残っていました。派生型は四則演算のほかに、べき乗の ** や単項の -、abs も受け継ぎます1。最初の型では Width ** 2 が px² を長さの型のまま返し、Right_Edge - Left_Edge を座標の変数に入れる式も通りました。前者はピクセルの長さどうしの掛け算と同じ誤りで、後者は長さを座標として扱う誤りです。
上のパッケージのように ** と座標を返す引き算も abstract で消すと、次の式はどれもコンパイルエラーになります。
with Vision_Units; use Vision_Units;
with X_Axis; use X_Axis;
procedure Err_Inherited_Ops is
Left_Edge : constant Position := 120.25;
Right_Edge : constant Position := 630.75;
Width : constant Length := 510.0;
Area : constant Length := Width ** 2; -- px² を px として持つ
Wrong_Pos : constant Position := Right_Edge - Left_Edge; -- 長さを座標として持つ
Mm2 : constant Millimeters := Millimeters'(3.0) ** 2; -- mm² を mm として持つ
begin
null;
end Err_Inherited_Ops;
err_inherited_ops.adb:9:46: error: cannot call abstract operation "**" declared at vision_units-axis.ads:21, instance at x_axis.ads:2
err_inherited_ops.adb:10:51: error: expected type "Position" defined at vision_units-axis.ads:4, instance at x_axis.ads:2
err_inherited_ops.adb:10:51: error: found type "Length" defined at vision_units-axis.ads:5, instance at x_axis.ads:2
err_inherited_ops.adb:11:58: error: cannot call abstract operation "**" declared at vision_units.ads:8
座標を返す引き算を消したので、Right_Edge - Left_Edge に使える演算子は長さを返すものだけになり、座標の変数には入れられません。消し忘れを防ぐには、型ごとに受け継ぐ演算子を並べ、結果の単位が合うかを1つずつ確かめます。
flowchart TB
accTitle: 取り違えとGNATのエラーの種類
accDescr: ピクセルの長さ同士の掛け算、座標同士の足し算、べき乗はabstractの演算子を呼んだエラー、係数の掛け忘れは型の不一致のエラー、座標の換算とx・yの取り違えと係数の向きの逆は演算子の引数の型が合わないエラーになることを示す。
A["px × px、座標 + 座標、**"] --> E1["cannot call abstract operation"]
B["係数の掛け忘れ"] --> E2["expected type … found type"]
C["座標の換算、x と y、係数の向き"] --> E3["invalid operand types for operator"]
図7: 消した演算子を呼ぶと abstract のエラー、定義していない組み合わせは引数の型のエラーとして報告される。
ゲージから校正係数を求めて幅を換算する
型を分けたあとの計算は次のようになります。10 mm のゲージを写した画像から校正係数を求め、部品の幅をミリメートルに直し、0.1 mm をピクセルに直してエッジを探す範囲を広げます。
with Ada.Text_IO; use Ada.Text_IO;
with Vision_Units; use Vision_Units;
with X_Axis; use X_Axis;
procedure Measure_Width is
-- 10 mm のゲージを写すと、x 方向に 500 px だった
Gauge_Mm : constant Millimeters := 10.0;
Gauge_Px : constant X_Axis.Length := 500.0;
Scale : constant Mm_Per_Px := Gauge_Mm / Gauge_Px;
-- 部品の左右のエッジの座標
Left_Edge : constant Position := 120.25;
Right_Edge : constant Position := 630.75;
Width_Px : constant X_Axis.Length := Right_Edge - Left_Edge;
Width_Mm : constant Millimeters := Width_Px * Scale;
-- 中点は「左端 + 長さの半分」で求める
Center : constant Position := Left_Edge + Width_Px / 2.0;
-- 0.1 mm を px にして、エッジを探す範囲を左へ広げる
Margin : constant X_Axis.Length := Millimeters'(0.1) * Invert (Scale);
Search_From : constant Position := Left_Edge - 2.0 * Margin;
begin
Put_Line ("scale =" & Mm_Per_Px'Image (Scale) & " mm/px");
Put_Line ("width =" & X_Axis.Length'Image (Width_Px) & " px");
Put_Line ("width =" & Millimeters'Image (Width_Mm) & " mm");
Put_Line ("center =" & Position'Image (Center) & " px");
Put_Line ("search =" & Position'Image (Search_From) & " px");
end Measure_Width;
scale = 2.00000000000000E-02 mm/px
width = 5.10500000000000E+02 px
width = 1.02100000000000E+01 mm
center = 3.75500000000000E+02 px
search = 1.10250000000000E+02 px
変数の型を宣言で書いておけば、右辺の演算子は型から選ばれます。Gauge_Mm / Gauge_Px は Millimeters / Length なので、結果は Mm_Per_Px です。抽象にした Length × Length は名前解決の候補にならないので3、2.0 * Margin は Long_Float × Length の演算子に一意に決まります。
flowchart TB
accTitle: 校正係数を求めてから換算する流れ
accDescr: ゲージのミリメートルをゲージのピクセルの長さで割ってmm/pxの係数を求め、部品の長さに掛けてミリメートルにし、係数の逆数をミリメートルに掛けてピクセルの余裕を求めることを示す。
G1["ゲージ 10 mm"] --> S["mm/px の係数"]
G2["ゲージ 500 px"] --> S
S --> W["幅 510.5 px × 係数 = 10.21 mm"]
S -->|"Invert"| I["px/mm の係数"]
I --> R["0.1 mm × px/mm = 余裕（px）"]
図8: 係数は既知の寸法から求め、ピクセルからミリメートルへは mm/px、逆向きは px/mm を使う。
公差の判定を浮動小数点数のまま比べない
換算までを型で守っても、判定で別の問題が起きます。図面が 5.00 ± 0.10 mm で、上限の 5.10 mm ちょうどを合格とする場合を考えます。0.01 mm/px の係数で 510 px を測ると、計算上はちょうど 5.10 mm です。測定値は前の節までと同じ Millimeters の型で計算し、これを Long_Float のまま上限と比べました。
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Long_Float_Text_IO; use Ada.Long_Float_Text_IO;
with Vision_Units; use Vision_Units;
with X_Axis; use X_Axis;
with Tolerance; use Tolerance;
procedure Tolerance_Check is
-- 図面は 5.00 ± 0.10 mm。上限の 5.10 mm ちょうどは合格
Drawing : constant Spec := (Nominal => 5.000, Minus => 0.100, Plus => 0.100);
procedure Judge (Px : Length; Scale : Mm_Per_Px) is
Measured : constant Millimeters := Px * Scale;
Upper : constant Long_Float :=
Long_Float (Drawing.Nominal) + Long_Float (Drawing.Plus);
begin
Put ("measured (Long_Float) = ");
Put (Long_Float (Measured), Fore => 1, Aft => 17, Exp => 0);
New_Line;
Put ("upper (Long_Float) = ");
Put (Upper, Fore => 1, Aft => 17, Exp => 0);
New_Line;
Put_Line ("Long_Float の比較 : " & Boolean'Image (Long_Float (Measured) <= Upper));
Put_Line ("Mm に丸めてから比較 : "
& Boolean'Image (Accept_Rounded (Measured, Drawing)));
end Judge;
-- 型変換は切り捨て、'Round は四捨五入
procedure Show_Conversion (X : Long_Float) is
begin
Put_Line ("Mm (X) =" & Mm'Image (Mm (X)));
Put_Line ("Mm'Round (X) =" & Mm'Image (Mm'Round (X)));
end Show_Conversion;
begin
Judge (Px => 510.0, Scale => 0.01);
Show_Conversion (5.0996);
end Tolerance_Check;
measured (Long_Float) = 5.10000000000000053
upper (Long_Float) = 5.09999999999999964
Long_Float の比較 : FALSE
Mm に丸めてから比較 : TRUE
Mm (X) = 5.099
Mm'Round (X) = 5.100
0.01 も 5.1 も2進の浮動小数点数では正確に表せないので、測定値は 5.10000000000000053、上限は 5.09999999999999964 になりました。上限ちょうどの部品が Long_Float の比較では不合格です。
測定値と上限を Judge の引数から計算したのは、510.0 * 0.01 のように定数だけで書くと誤差が見えなくなるためです。Ada の静的な式はコンパイル時に正確な値で計算され、最後に1回だけ丸められます6。そこで実際の検査と同じように、実行時に渡す値で計算しました。
flowchart TB
accTitle: 浮動小数点数のまま比べたときの判定
accDescr: 510ピクセルに0.01を掛けた測定値が5.10000000000000053、5.00と0.10を足した上限が5.09999999999999964になり、そのまま比べると上限ちょうどの部品が不合格になり、0.001ミリメートル刻みに丸めると合格になることを示す。
A["510 px × 0.01 mm/px"] --> M["5.10000000000000053"]
B["5.00 mm + 0.10 mm"] --> U["5.09999999999999964"]
M --> C{"Long_Float で比べる"}
U --> C
C --> NG["不合格"]
M --> R["0.001 mm 刻みに丸める"]
R --> OK["5.100 mm で合格"]
図9: 上限ちょうどの測定値を浮動小数点数のまま比べると上限を超え、図面の桁に丸めると合格になる。
10進固定小数点型で図面の桁にそろえる
判定には図面の桁で値を持つ10進固定小数点型を使いました。type Mm is delta 0.001 digits 7; は、0.001 mm 刻みで7桁、つまり -9999.999〜9999.999 mm を表す型です。10進固定小数点型では値の刻み（small）が delta と同じで、delta は10のべき乗に限られます7。0.100 や 5.100 は刻みの整数倍なので、誤差なく表せます。
with Vision_Units;
package Tolerance is
-- 0.001 mm 刻みの10進固定小数点型（-9999.999 .. 9999.999 mm）
type Mm is delta 0.001 digits 7;
type Spec is record
Nominal : Mm;
Minus : Mm;
Plus : Mm;
end record;
-- 下限と上限を含めて合格とする
function Accept_Fixed (Measured : Mm; S : Spec) return Boolean is
(Measured in S.Nominal - S.Minus .. S.Nominal + S.Plus);
-- ミリメートルの測定値を図面の桁に丸めてから判定する
function Accept_Rounded (Measured : Vision_Units.Millimeters; S : Spec) return Boolean is
(Accept_Fixed (Mm'Round (Measured), S));
end Tolerance;
浮動小数点数の測定値を Mm に直すときは、型変換と 'Round の違いに気を付けます。10進固定小数点型への型変換は、値が刻みの倍数でなければ0の方向へ切り捨てます8。'Round は最も近い刻みの倍数に丸め、ちょうど中間なら0から遠いほうを選びます9。前の節の出力で、5.0996 は型変換で 5.099、Mm'Round で 5.100 になりました。上の例の 5.10000000000000053 も、Mm'Round で 5.100 になって合格と判定されています。
丸めてから比べるので、上限 5.100 mm の判定では 5.1005 mm 未満の測定値まで合格になります。刻みの半分までを合格に含めるという判定の方針です。図面の公差に対してこれでよいかは、あらかじめ決めておきます。また、Mm'Round は結果が Mm の範囲（±9999.999）を外れると Constraint_Error になります。
Accept_Rounded の引数の型は Millimeters にしました。引数が Long_Float だと、型付きの値を渡すには Long_Float (…) の型変換が要り、ピクセルの長さも同じ書き方で渡せてしまいます。引数を Millimeters にすると、ピクセルの長さを渡す呼び出しは expected type "Millimeters" のコンパイルエラーになりました。'Round は Millimeters の値にもそのまま使えます。
flowchart TB
accTitle: 10進固定小数点型への型変換と'Round
accDescr: 浮動小数点数の5.0996を10進固定小数点型Mmに直すとき、型変換は0の方向へ切り捨てて5.099、'Roundは最も近い倍数に丸めて5.100になることを示す。
X["5.0996（Long_Float）"] -->|"Mm（X）"| T["5.099（0 の方向へ切り捨て）"]
X -->|"Mm'Round（X）"| R["5.100（最も近い倍数）"]
図10: 10進固定小数点型への型変換は切り捨て、’Round は四捨五入になる。
10進ではない普通の固定小数点型は、delta だけを書くと、刻みを delta 以下の2のべき乗から処理系が選びます7。Small を指定すれば、刻みを 0.001 にできます。
with Ada.Text_IO; use Ada.Text_IO;
procedure Small_Check is
-- delta だけを書くと、small は delta 以下の2のべき乗になる
type Mm_Binary is delta 0.001 range -1000.0 .. 1000.0;
-- small を指定すると、0.001 の倍数をそのまま表せる
type Mm_Exact is delta 0.001 range -1000.0 .. 1000.0
with Small => 0.001;
A : constant Mm_Binary := 0.1;
B : constant Mm_Exact := 0.1;
begin
Put_Line ("Mm_Binary'Small =" & Long_Float'Image (Mm_Binary'Small));
Put_Line ("Mm_Exact'Small =" & Long_Float'Image (Mm_Exact'Small));
Put_Line ("Mm_Binary 0.1 =" & Long_Float'Image (Long_Float (A)));
Put_Line ("Mm_Exact 0.1 =" & Long_Float'Image (Long_Float (B)));
end Small_Check;
small_check.adb:11:30: warning: static fixed-point value is not a multiple of Small [-gnatwb]
Mm_Binary'Small = 9.76562500000000E-04
Mm_Exact'Small = 1.00000000000000E-03
Mm_Binary 0.1 = 9.96093750000000E-02
Mm_Exact 0.1 = 1.00000000000000E-01
GNAT 13.3.0 と 16.1.0 は、どちらも Mm_Binary の刻みを 2⁻¹⁰（0.0009765625）にし、0.1 は 0.099609375 になりました。警告をすべて出す -gnatwa（または -gnatwb）を付けてコンパイルすると、0.1 が刻みの倍数でないという警告が出ます。既定のスイッチでは出ません。図面の値を正確に持ちたいなら、10進固定小数点型を使うか、Small を指定します。
flowchart TB
accTitle: 固定小数点型の刻みの決まり方
accDescr: 10進固定小数点型は刻みがdeltaと同じ10のべき乗になり、普通の固定小数点型はdeltaだけを書くと2のべき乗の刻みになって0.1を正確に表せず、Smallを指定すると0.001の刻みにできることを示す。
D["delta 0.001 digits 7（10進）"] --> D1["刻み 0.001"]
O["delta 0.001 range …（普通）"] --> O1["刻み 2⁻¹⁰（GNAT 13 と 16）"]
O1 --> O2["0.1 が 0.099609375 になる"]
S["普通の型 + Small => 0.001"] --> S1["刻み 0.001"]
図11: 図面の桁で値を持つには、10進固定小数点型か、Small を指定した固定小数点型を使う。
換算までは Long_Float の派生型で計算し、判定の直前に Mm'Round で図面の桁にそろえるという分け方にしました。サブピクセルのエッジ位置のように細かい値は浮動小数点数で計算し、合否を決める比較だけを固定小数点で行います。
GNAT の次元系で次元を検査する
GNAT には浮動小数点型に次元を持たせる独自の仕組みがあります。型に Dimension_System アスペクトで基本の次元を宣言し、subtype に Dimension アスペクトで次元の組み合わせを付けると、式の次元が合わないときにコンパイルエラーになります1011。Ada の規格にはない機能なので、GNAT 以外のコンパイラーでは使えません。GNAT は SI の7つの基本単位で作った System.Dim.Mks も用意しています。
寸法検査用に、ミリメートルと x 方向・y 方向のピクセルを基本の次元にした型を作りました。
package Vision_Dims is
-- GNAT 独自のアスペクト。mm と x・y のピクセルを基本の次元にする
type Vision_Type is new Long_Float
with Dimension_System =>
((Unit_Name => Millimeter, Unit_Symbol => "mm", Dim_Symbol => 'L'),
(Unit_Name => Pixel_X, Unit_Symbol => "pxX", Dim_Symbol => 'X'),
(Unit_Name => Pixel_Y, Unit_Symbol => "pxY", Dim_Symbol => 'Y'));
subtype Mm_Length is Vision_Type
with Dimension => (Symbol => "mm", Millimeter => 1, others => 0);
subtype X_Length is Vision_Type
with Dimension => (Symbol => "pxX", Pixel_X => 1, others => 0);
subtype Y_Length is Vision_Type
with Dimension => (Symbol => "pxY", Pixel_Y => 1, others => 0);
subtype X_Scale is Vision_Type
with Dimension =>
(Symbol => "mm/pxX", Millimeter => 1, Pixel_X => -1, others => 0);
subtype Y_Scale is Vision_Type
with Dimension =>
(Symbol => "mm/pxY", Millimeter => 1, Pixel_Y => -1, others => 0);
pragma Warnings (Off, "*assumed to be*");
mm : constant Mm_Length := 1.0;
pxX : constant X_Length := 1.0;
pxY : constant Y_Length := 1.0;
pragma Warnings (On, "*assumed to be*");
end Vision_Dims;
with Ada.Text_IO; use Ada.Text_IO;
with System.Dim.Float_IO;
with Vision_Dims; use Vision_Dims;
procedure Dim_Check is
package Vision_IO is new System.Dim.Float_IO (Vision_Type);
use Vision_IO;
Scale_X : constant X_Scale := 10.0 * mm / (500.0 * pxX);
Width : constant X_Length := 510.5 * pxX;
Width_Mm : constant Mm_Length := Width * Scale_X;
begin
Put (Scale_X, Aft => 4, Exp => 0);
New_Line;
Put (Width_Mm, Aft => 3, Exp => 0);
New_Line;
end Dim_Check;
0.0200 mm/pxX
10.210 mm
System.Dim.Float_IO で出力すると、値の後ろに次元の記号が付きます。次元が合わない式は次のように報告されました。
with Vision_Dims; use Vision_Dims;
procedure Err_Dim is
Scale_X : constant X_Scale := 10.0 * mm / (500.0 * pxX);
Width : constant X_Length := 510.0 * pxX;
Height : constant Y_Length := 300.0 * pxY;
Area : constant X_Length := Width * Width; -- px × px
Forgot : constant Mm_Length := Width; -- 係数の掛け忘れ
Mixed : constant Mm_Length := Height * Scale_X; -- x と y
Inverse : constant Mm_Length := Width * (1.0 / Scale_X); -- 係数の向き
begin
null;
end Err_Dim;
err_dim.adb:8:04: error: dimensions mismatch in object declaration
err_dim.adb:8:42: error: expected dimension [X], found [X**2]
err_dim.adb:9:04: error: dimensions mismatch in object declaration
err_dim.adb:9:36: error: expected dimension [L], found [X]
err_dim.adb:10:04: error: dimensions mismatch in object declaration
err_dim.adb:10:43: error: expected dimension [L], found [L.X**(-1).Y]
err_dim.adb:11:04: error: dimensions mismatch in object declaration
err_dim.adb:11:42: error: expected dimension [L], found [L**(-1).X**2]
4つの取り違えがどれも次元の不一致として報告されました。[L] はミリメートル、[X] と [Y] は x 方向と y 方向のピクセルの次元です。
次元系では掛け算と割り算の結果の次元をコンパイラーが計算します。px × px は禁止されず、次元 [X**2] の値として扱われるので、面積として使うこともできます。mm/px と px/mm は次元の指数の符号で区別されます。演算子を1つずつ定義する必要はありません。
一方で、次元系では座標と長さを区別できません。どちらも次元は [X] だからです。
flowchart TB
accTitle: 演算子を定義する方法と次元系で防げる取り違え
accDescr: 派生型と演算子を定義する方法はpx×px、係数の掛け忘れ、座標の換算、xとyの取り違え、係数の向きの逆を防ぎ、GNATの次元系は座標の換算以外の取り違えを防ぎ、面積は次元X**2として計算できることを示す。
T["派生型 + 演算子の定義"] --> T1["5つの取り違えを防ぐ"]
T1 --> T2["演算子を1つずつ書く"]
D["GNAT の次元系"] --> D1["座標の換算以外の4つを防ぐ"]
D1 --> D2["面積は X**2 として計算できる"]
D2 --> D3["GNAT でしか使えない"]
図12: 次元系は演算子を書かずに次元を検査できるが、座標と長さの区別と、GNAT 以外での利用はできない。
座標と長さを区別したい場合や、GNAT 以外のコンパイラーでもビルドしたい場合は、前半の派生型と演算子の方法を選びます。
換算の結果が型の範囲からはみ出さないことを SPARK で証明する
型で単位をそろえても、値が型の範囲に収まるかは別の問題です。前半の型は Long_Float の派生型なので、範囲を決めていません。範囲を持つ固定小数点型で換算を書き、範囲検査が失敗しないことを SPARK の GNATprove で証明しました。SPARK は Ada のサブセットで、GNATprove は SPARK で書いたコードの性質を証明するツールです。詳しくは SPARKによる形式検証入門 にあります。
package Scaled_Length with SPARK_Mode is
-- 0.01 px 刻みの長さ。画像の幅は 16384 px まで
type Px_Length is delta 0.01 range 0.0 .. 16_384.0
with Small => 0.01;
-- 0.00001 mm/px 刻みの校正係数
type Mm_Per_Px is delta 0.000_01 range 0.000_01 .. 1.0
with Small => 0.000_01;
-- 0.001 mm 刻みの長さ
type Mm is delta 0.001 range -100_000.0 .. 100_000.0
with Small => 0.001;
function To_Mm (L : Px_Length; S : Mm_Per_Px) return Mm;
end Scaled_Length;
package body Scaled_Length with SPARK_Mode is
function To_Mm (L : Px_Length; S : Mm_Per_Px) return Mm is
begin
return Mm (L * S);
end To_Mm;
end Scaled_Length;
固定小数点型どうしの掛け算の結果は universal_fixed という型になり、結果の型は文脈か型変換で決まります12。ここでは型変換で Mm (L * S) と明示し、Mm に変換するときに範囲検査が入ります。長さは最大 16384 px、係数は最大 1.0 mm/px なので、積は最大 16384 mm で、Mm の範囲に収まります。
GNATprove に --level=2 --report=all --checks-as-errors=on を付けて実行すると13、L * S のオーバーフロー検査、Mm への範囲検査、To_Mm が必ず終わることの3件が証明されました。
info: overflow check proved
--> scaled_length.adb:5:20
info: range check proved
--> scaled_length.adb:5:20
info: implicit aspect Always_Terminates on "To_Mm" has been proved, subprogram will terminate
--> scaled_length.ads:15:13
Success: all checks proved (3 checks).
この証明が示すのは、結果が Mm の範囲に収まることだけで、値の丸め方は扱っていません。10進ではない固定小数点型への型変換について、規格は変換先の型の精度の範囲の値になるとしか決めていません8。手元の GNAT 13.3.0 では切り捨てになり、0.19 px × 0.01 mm/px（0.0019 mm）は 0.001 mm、510.55 px × 0.01999 mm/px（10.2058945 mm）は 10.205 mm になりました。結果は最大で 0.001 mm 小さくなるので、判定に使うなら前の節のように丸め方を決めておきます。
次に、画像の幅の上限を 1000000 px に広げたパッケージを用意しました。違いは Px_Length の範囲だけです。
-- 画像の幅の上限を 1000000 px に広げた場合
type Px_Length is delta 0.01 range 0.0 .. 1_000_000.0
with Small => 0.01;
このパッケージでは、積が最大 1000000 mm になって Mm の範囲を超えます。GNATprove は範囲検査を証明できず、high の重要度で「失敗するかもしれない」と報告しました。
high: range check might fail, cannot prove upper bound for L * S
--> scaled_length.adb:5:20
5 | return Mm (L * S);
| ~~^~~
+ e.g. when L = 1000000
and S = 10001/100000
+ reason for check: result of fixed-point multiplication must be convertible to the target type of the conversion
+ possible fix: subprogram at scaled_length.ads:15 should mention L and S in a precondition
--> scaled_length.ads:15:04
15 | function To_Mm (L : Px_Length; S : Mm_Per_Px) return Mm;
| ^
+ provers reached time limit before completing the proof
e.g. の行は検査が失敗する値の例です。L = 1000000 px、S = 0.10001 mm/px なら、積は 100010 mm で Mm の上限を超えます。possible fix の行は To_Mm の事前条件で L と S の範囲を絞る直し方を示しています。--checks-as-errors=on を付けているので、証明できない検査が残ると GNATprove は終了コード1で終わりました。
GNATprove を使わない通常のビルドでは、この誤りは実行時に初めて分かります。引数の長さと係数で To_Mm を呼ぶ小さなプログラム（記事には載せていません）で広げたパッケージを試すと、16384 px では値を返し、1000000 px では Constraint_Error で止まりました。
$ ./bin/wide_run 16384.0 1.0
16384.000
$ ./bin/wide_run 1000000.0 1.0
raised CONSTRAINT_ERROR : scaled_length.adb:5 range check failed
flowchart TB
accTitle: 型の範囲から換算の結果を証明する
accDescr: 長さの上限16384ピクセルと係数の上限1.0から積の上限16384ミリメートルが決まり、Mmの範囲に収まるので証明でき、長さの上限を1000000ピクセルに広げると積がMmの範囲を超えて証明できず、実行時にはConstraint_Errorになることを示す。
A["長さ ≤ 16384、係数 ≤ 1.0"] --> B["積 ≤ 16384 mm"]
B --> C["Mm の範囲内なので証明できる"]
W["長さの上限を 1000000 に"] --> X["積 ≤ 1000000 mm"]
X --> Y["Mm の範囲を超え、証明できない"]
Y -.-> Z["実行時に Constraint_Error"]
図13: GNATprove は型の範囲から積の範囲を求め、変換先の型に収まらない可能性があれば報告する。
C# と F# での同じ考え方
C# ではピクセルの長さやミリメートルを readonly record struct などの別の型にし、意味のある演算子だけを定義できます14。新しく作った構造体には算術の演算子がないので、Ada のように受け継いだ演算子を消す手順は要りません。x 用と y 用の型は、軸を表す目印の型を総称型の型引数に渡せば1つの定義から作れるはずですが、この記事では試していません。図面の桁で比べる用途には、10進の浮動小数点数である decimal 型が使えます15。F# には言語の機能として単位（units of measure）があり、GNAT の次元系と同じように単位の組み合わせを検査できます16。
型では防げないこと
型が検査するのは、値の種類と演算の組み合わせだけです。次のような誤りは型を分けても残ります。
- 校正係数の値そのものの誤り。ゲージの寸法を打ち間違えた、ゲージの写った位置がずれていた、などです。
- レンズのゆがみや斜めからの撮影で、1つの係数では換算できない場合。画像の場所によって係数が変わるなら、座標から係数を求める補正が別に要ります。
- 外部のライブラリとの境界。エッジ検出のライブラリが返す
doubleをPositionに変換する箇所は、どの軸の座標かを人が決めます。型変換を書く箇所を1か所にまとめ、レビューの対象にします。 - 型のないリテラル。
2.0のような数値のリテラルは、式が解決できる型になります。Width_Px * 2.0では 2.0 が mm/px の係数になり、Millimeters'(1.0) * 50.0では 50.0 が px/mm の係数になりました。y 方向の長さに x 方向の係数の値をリテラルで書いても、y の係数として通ります。どれも-gnatwaを付けて警告なしにコンパイルできました。係数は名前と型の付いた定数にし、式にリテラルの係数を直接書かないようにします。
flowchart TB
accTitle: 型で防げることと防げないこと
accDescr: 型は値の種類と演算の組み合わせの誤りを防ぐが、校正係数の値の誤り、レンズのゆがみによる係数の変化、外部ライブラリの値を受け取る箇所での軸の取り違え、型のないリテラルで書いた係数は防げないことを示す。
T["型の検査"] --> OK["値の種類と演算の組み合わせ"]
T -.-> NG["型では検査できない"]
NG -.-> N1["係数の値の誤り"]
NG -.-> N2["場所で変わる係数"]
NG -.-> N3["境界での変換"]
NG -.-> N4["型のないリテラルの係数"]
図14: 型は演算の組み合わせを検査するが、値の正しさと、外から値を受け取る箇所の判断は人が確かめる。
試した環境と確かめていないこと
- コンパイル、実行、エラーメッセージは、2026年11月10日に手元の Ubuntu 24.04 の GNAT 13.3.0（Ubuntu のパッケージ）と gprbuild で確かめました。コンパイラーのスイッチは
-gnat2022 -gnatwaです。GitHub Actions の Ubuntu 24.04 のランナーでも、Alire 2.1.1 が用意した GNAT 16.1.0 で同じコードをビルドして実行し、エラーメッセージと出力が同じになることを確かめました。ほかのバージョンの GNAT では、メッセージの文言や列の番号が変わることがあります。 Mm_Binaryの刻みが 2⁻¹⁰ になったのは GNAT 13.3.0 と 16.1.0 での結果です。規格は「delta 以下の2のべき乗」としか決めていません。- GNATprove の証明は GitHub Actions の Ubuntu 24.04 のランナーで GNATprove FSF 16.1.0（Why3 1.8.2+git、Alt-Ergo 2.6.1、cvc5 1.3.2、Z3 4.15.4）を使い、
--level=2で行いました。手元の GNAT 13.3.0 には GNATprove が入っていません。 - 実際のカメラの画像、エッジ検出のライブラリとの組み合わせ、Windows でのビルドは試していません。
- 検証に使ったプロジェクト一式は公開しておらず、記事のコードはその抜粋です。
関連記事
この記事はシリーズ「Ada とマシンビジョン」の1本です。シリーズのほかの記事は次のとおりです。
- 画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較
- GigE VisionのパケットをAdaの型で受ける ── 表現句の落とし穴とSPARKで証明するパーサー
- 取りこぼさない取り込み処理をAdaのタスクで作る ── 保護オブジェクトのリングバッファと優先度
- Adaの検査ロジックをC#の検査アプリから呼ぶ ── 画像バッファをコピーせずに渡し、境界で守る
関係する既存の記事は次のとおりです。
- Ada言語の魅力 ── 型で設計を語り、数十年動き続けるソフトウェアを支える言語
- Adaのジェネリックプログラミング ── 型で契約を書き、再利用をゼロコストで実現する
- SPARKによる形式検証入門 ── Adaの契約から数学的証明へ
- GigE Vision・USB3 Visionカメラの取りこぼし ── 原因の切り分けとWindows側の設定
参考リンク
-
Ada Reference Manual (Ada 2022), 3.4 Derived Types and Classes. 派生型が親の型の基本演算を受け継ぐこと。 ↩ ↩2
-
Ada Reference Manual (Ada 2022), 3.9.3 Abstract Types and Subprograms. 抽象サブプログラムは本体を持たず、ディスパッチしない呼び出しが禁止されること。 ↩
-
Ada Reference Manual (Ada 2022), 6.4 Subprogram Calls. 呼び出しの名前は、ディスパッチするものでない限り抽象サブプログラムに解決されないこと（8/2項）。 ↩ ↩2
-
Ada Reference Manual (Ada 2022), 6.6 Overloading of Operators. 演算子の名前の関数を宣言できること。 ↩
-
Ada Reference Manual (Ada 2022), 12.3 Generic Instantiation. インスタンスが総称単位の写しとして宣言されること。 ↩
-
Ada Reference Manual (Ada 2022), 4.9 Static Expressions and Static Subtypes. 静的な式が正確に計算され、実数の結果は最後に機械の表現へ丸められること。 ↩
-
Ada Reference Manual (Ada 2022), 3.5.9 Fixed Point Types. 普通の固定小数点型の small が delta 以下の2のべき乗から処理系によって選ばれること、10進固定小数点型の small が delta と等しく delta が10のべき乗であること。 ↩ ↩2
-
Ada Reference Manual (Ada 2022), 4.6 Type Conversions. 10進固定小数点型への型変換で、値が small の倍数でなければ0の方向へ切り捨てられること（31項）と、それ以外の実数型への変換の結果が変換先の型の精度の範囲の値になること（32項）。 ↩ ↩2
-
Ada Reference Manual (Ada 2022), 3.5.10 Operations of Fixed Point Types.
'Roundが最も近い small の倍数に丸め、中間なら0から遠いほうを選ぶこと。 ↩ -
AdaCore, GNAT User’s Guide: GNAT and Program Execution. 「Performing Dimensionality Analysis in GNAT」で、Dimension_System と Dimension による次元の検査と
System.Dim.Mks。 ↩ -
AdaCore, GNAT Reference Manual: Implementation Defined Aspects. Dimension と Dimension_System が GNAT の処理系定義のアスペクトであること。 ↩
-
Ada Reference Manual (Ada 2022), 4.5.5 Multiplying Operators. 固定小数点型どうしの掛け算が universal_fixed を返し、結果の型が文脈か型変換で決まること。 ↩
-
AdaCore, SPARK User’s Guide: How to Run GNATprove.
--level、--report、--checks-as-errorsなどのオプション。 ↩ -
Microsoft Learn, Operator overloading - predefined unary, arithmetic, equality, and comparison operators. C# の型に演算子を定義する方法。 ↩
-
Microsoft Learn, Floating-point numeric types.
decimal型の範囲と精度。 ↩ -
Microsoft Learn, Units of Measure. F# の単位の宣言と検査。 ↩
関連する記事
同じタグを共有する最新の記事です。さらに近い話題で知識を深められます。
取りこぼさない取り込み処理をAdaのタスクで作る ── 保護オブジェクトのリングバッファと優先度
カメラの画像を取り込む処理を、Adaの周期タスク、保護オブジェクトで作るリングバッファ、優先度で組み立てます。処理が遅いときに捨てた数と待ち時間を測り、Linuxで優先度が効く条件とSPARKで確かめられる範囲を書きます。
GigE VisionのパケットをAdaの型で受ける ── 表現句の落とし穴とSPARKで証明するパーサー
GigE Visionの画像を運ぶGVSPのヘッダーを、Adaの表現句とScalar_Storage_Orderで型に対応させる方法と落とし穴を説明します。壊れたパケットでも範囲外を読まないパーサーを書き、SPARKで証明します。
Adaの検査ロジックをC#の検査アプリから呼ぶ ── 画像バッファをコピーせずに渡し、境界で守る
WPFの検査アプリはそのままに、合否を決める処理だけをAdaのDLLにする方法を、Cと.NETのコンソールアプリから実際に呼んで説明します。画像をコピーせずに渡し、寸法を確かめ、結果とエラーコードを返す境界の作り方が中心です。
画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較
画像処理のコードが画像の外を読み書きしないことを、SPARKのGNATproveで証明します。2値化、3×3の平滑化、ラベリングを例に、証明の書き方と証明していない範囲、検査を外したときのCとの速度の差を実測でまとめます。
Alire で Ada のプロジェクトを始める ── プロジェクト作成、依存の追加、ビルドプロファイル、GNATproveまで
AdaのパッケージマネージャーAlireで、プロジェクトの作成、GNATの自動取得、依存クレートの追加、ビルドプロファイルの切り替え、GNATproveによる証明までを、alr 2.1で実行した出力とともに説明します。
関連トピック
このテーマと近いトピックページです。記事を起点に、関連するサービスや他の記事へ進めます。
Windows技術トピック
Windows 開発、不具合調査、既存資産活用の技術トピックをまとめた入口です。
不具合調査 / 長期稼働テーマ
再現しにくい不具合、通信停止、長期稼働障害、失敗パス検証を整理するトピックです。
このテーマがつながるサービス
この記事は次のサービスページにつながります。近い入口からご覧ください。
技術相談・設計レビュー
検査アプリの計算で、ピクセル、ミリメートル、校正係数をどの型で表し、どこで換算するかを整理したい場合に、技術相談・設計レビューとして扱えます。
Windowsアプリ開発
画像で寸法を測る検査アプリの判定部分を、単位の取り違えがコンパイル時に分かる形で作りたい場合に、Windowsアプリ開発の一部として扱えます。
よくある質問
この記事のテーマについて、相談時によくある質問をまとめています。
- Adaでピクセルとミリメートルを別の型にすれば、単位の取り違えはすべて防げますか？
- 派生型にするだけでは足りません。派生型は親の型の演算子を受け継ぐので、ピクセルの長さどうしの掛け算がピクセルの長さを返します。意味のない演算子をabstractで宣言し直して呼べなくし、長さ×校正係数→ミリメートルのような意味のある演算子だけを定義します。
- x方向とy方向の校正係数の取り違えも型で防げますか？
- 防げます。座標、長さ、校正係数の型を総称パッケージの中で宣言し、x用とy用に2回インスタンス化すると、インスタンスごとに別の型になります。y方向の長さにx方向の係数を掛ける式は、GNATでコンパイルエラーになりました。
- 公差の判定を浮動小数点数で行うと何が困りますか？
- 上限ちょうどの値が不合格になることがあります。0.01 mm/pxで510 pxを測ると、Long_Floatの計算では5.10000000000000053になり、5.10 mmの上限を超えました。測定値を0.001 mm刻みの10進固定小数点型に丸めてから比べると、合格と判定できます。