Separating Pixels and Millimeters with Types — Preventing Unit Mix-ups in Dimensional Inspection with Ada

In a program that measures part dimensions from images, pixel (px) values and millimeter (mm) values flow through the same calculations. Both are often held as floating-point numbers such as double, so the compiler gives no error and no warning when you forget to apply the calibration factor or multiply a y-direction length by the x-direction factor. The mistake is found only when the pass/fail decision goes wrong.

In Ada you can make image positions, pixel lengths, millimeters and calibration factors (mm/px) separate types and keep only the meaningful operations. This article lists the unit mix-ups that commonly occur in dimensional inspection and explains how to build types that turn each of them into a compile error, together with the errors GNAT actually produced. The second half covers why to use a decimal fixed-point type for tolerance checks and GNAT’s own dimension system. Finally, it proves with SPARK that the result of the conversion stays within the range of its type.

Compilation and execution were done on November 10, 2026 with GNAT 13.3.0 on my own Ubuntu 24.04 machine, and the error messages and outputs in this article are the results of those runs.

The proofs with GNATprove were done on a GitHub Actions Ubuntu 24.04 runner with GNAT 16.1.0 and GNATprove FSF 16.1.0 installed by Alire 2.1.1. On the same runner I also built and ran the other examples and confirmed that the error messages and outputs matched those on my machine.

The basics of derived types are explained in The Appeal of the Ada Language and How Ada and Rust Think About Safety, so this article starts from what dimensional inspection needs.

Where units get mixed up in dimensional inspection

From edge detection to the pass/fail decision, the unit of the value changes in this order. Edge detection returns positions in the image (px), and the difference between two positions is a length (px). Multiplying the length by the calibration factor (mm/px) gives a length in millimeters, which is finally compared with the drawing tolerance.

flowchart TB
        accTitle: The order in which the unit of the value changes in dimensional inspection
        accDescr: Shows the flow of taking the difference of the positions returned by edge detection to get a length, multiplying it by the calibration factor to get millimeters, and comparing it with the drawing tolerance to decide pass or fail.
        A["Image"] -->|"Detect edges"| B["Edge positions (px)"]
        B -->|"Take the difference of 2 points"| C["Length (px)"]
        C -->|"Multiply by the calibration factor (mm/px)"| D["Length (mm)"]
        D -->|"Compare with the drawing tolerance"| E["Pass/fail"]

Figure 1: Between the edge positions and the pass/fail decision, the value changes from a position to a pixel length and then to a millimeter length.

The following mix-ups occur in this flow. If all the values are floating-point numbers, every one of them compiles.

• Multiplying two pixel lengths and treating the area (px²) as a length.
• Forgetting to apply the calibration factor and sending a pixel length to the decision as millimeters.
• Forgetting to take the difference and converting an edge position as if it were a length.
• Multiplying a y-direction length by the x-direction calibration factor (the factors for x and y can differ because of the pixel aspect ratio or the optics).
• Reversing the direction of the calibration factor (confusing a mm/px factor with a px/mm factor).

flowchart TB
        accTitle: The stages where mix-ups occur
        accDescr: Shows that at the position stage the error is converting a position as if it were a length, at the length stage the errors are making an area into a length by multiplication and forgetting the factor, and at the stage of applying the factor the errors are confusing x and y and reversing the direction of the factor.
        B["Edge positions (px)"] --> C["Length (px)"]
        C --> D["Length (mm)"]
        B -.-> M1["Convert a position as if it were a length"]
        C -.-> M2["Treat px × px as a length"]
        C -.-> M3["Forget the calibration factor"]
        D -.-> M4["Confuse the x and y factors"]
        D -.-> M5["Reverse mm/px and px/mm"]

Figure 2: The five mix-ups occur at three stages: positions, pixel lengths, and the conversion to millimeters.

In the diagram a solid line marks a relation that always holds and a dashed line marks a conditional one (the conditions are given per relation on the detail page). The full list of relations (10 in total, with evidence and certainty) and the definitions of the main concepts are collected on the knowledge map detail page (in Japanese). Data: JSON-LD / Turtle

A derived type alone still lets px × px through

When you write type Px_Length is new Long_Float; in Ada, you get a separate type derived from Long_Float. Because it is a separate type, assigning a Px_Length value directly to a Mm_Length variable is a compile error. However, a derived type inherits the primitive operations of its parent type¹. Multiplication of Long_Float returns Long_Float, so multiplication of Px_Length returns 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 becomes px
   Scale : constant Px_Length := 0.01;           --  a value meant as 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;

This program compiled without warnings and printed the following.

 2.60100000000000E+05
 5.10000000000000E+00

The expression that puts an area into a length type goes through. The calibration factor line also has a problem. The factor is declared as Px_Length because making it a separate type would make Width * Scale impossible to write. To calculate while keeping the types separate, you need type conversions such as Mm_Length (Long_Float (Width) * Long_Float (Scale)). Type checking does not apply where a type conversion is written, so the more conversions you stack up, the less point there is in separating the types.

flowchart TB
        accTitle: Operators inherited by a derived type
        accDescr: Shows that Px_Length derived from Long_Float inherits the four arithmetic operations as they are, that multiplying two Px_Length values returns Px_Length, and that making the factor a separate type requires type conversions.
        F["Long_Float"] -->|"type … is new"| P["Px_Length"]
        P --> O["Inherits the four arithmetic operations as they are"]
        O --> A["px × px returns Px_Length"]
        P -.-> S["A factor of another type cannot be multiplied"]
        S -.-> C["Writing conversions disables the check"]

Figure 3: A derived type is a separate type, but it also inherits the parent type’s operators, so meaningless multiplication goes through.

Removing meaningless operators with abstract

An inherited operator can no longer be called once it is redeclared with is abstract in the specification of the package that declares the type. This is because a non-dispatching call to an abstract subprogram, which has no body, is a compile error². A non-dispatching abstract subprogram is not even a candidate in name resolution³. On top of that, you define only the meaningful operators yourself. In Ada you can declare functions whose names are operator symbols, and each combination of parameter and result types is treated as a separate function⁴.

The millimeter type was written as follows.

package Vision_Units is

   type Millimeters is new Long_Float;

   --  mm × mm, mm ÷ mm and powers of mm returned as mm are meaningless, so remove them
   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;

   --  Scaling up or down is written with a dimensionless number
   function "*" (Left : Long_Float; Right : Millimeters) return Millimeters;
   function "/" (Left : Millimeters; Right : Long_Float) return Millimeters;

end Vision_Units;

Addition, subtraction and comparison are kept. Adding two millimeter values gives millimeters, so the inherited operators make sense as they are. For multiplication and division, the operations that take two millimeter values and also return millimeters are removed, and only operations with a dimensionless Long_Float operand are defined. The exponentiation operator ** is also inherited from Long_Float, but it returns mm² as mm, so it is removed as well.

flowchart TB
        accTitle: Operators kept and removed for Millimeters
        accDescr: Shows that addition, subtraction and comparison of Millimeters are kept as inherited, that multiplication and division of two Millimeters values and exponentiation are removed with abstract, and that multiplication and division with Long_Float are newly defined.
        M["Millimeters"] --> K["Keep: +, −, comparison"]
        M --> X["Remove (abstract): mm × mm, mm ÷ mm, mm ** n"]
        M --> N["Define: number × mm, mm ÷ number"]

Figure 4: Operators whose result unit is right are kept, the others are removed with abstract, and only the needed combinations are defined.

Building the pixel types per axis with a generic package

The pixel side needs four types: position, length, and calibration factors in two directions. To prepare them separately for the x and y directions, the types and operators are put into a generic package, which is instantiated twice, once for x and once for y. An instance is a copy of the generic package, and the types declared in it are separate types in each instance⁵.

generic
package Vision_Units.Axis is

   type Position  is new Long_Float;  --  position in the image (px)
   type Length    is new Long_Float;  --  length between 2 points (px)
   type Mm_Per_Px is new Long_Float;  --  calibration factor (mm/px)
   type Px_Per_Mm is new Long_Float;  --  its reciprocal (px/mm)

   --  Adding, multiplying and dividing positions is meaningless, so remove them
   function "+" (Left, Right : Position) return Position is abstract;
   function "*" (Left, Right : Position) return Position is abstract;
   function "/" (Left, Right : Position) return Position is abstract;

   --  Subtraction returning a position and exponentiation are meaningless for positions too
   function "-" (Left, Right : Position) return Position is abstract;
   function "**" (Left : Position; Right : Integer) return Position is abstract;

   --  Also remove operations that return px × px or powers of px as 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;

   --  Also remove multiplication, division and exponentiation of calibration factors
   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;

   --  Relations between positions and lengths
   function "-" (Left, Right : Position) return Length;
   function "+" (Left : Position; Right : Length) return Position;
   function "-" (Left : Position; Right : Length) return Position;

   --  Scaling a length up or down
   function "*" (Left : Long_Float; Right : Length) return Length;
   function "/" (Left : Length; Right : Long_Float) return Length;

   --  Unit conversion only in these two directions
   function "*" (Left : Length; Right : Mm_Per_Px) return Millimeters;
   function "*" (Left : Millimeters; Right : Px_Per_Mm) return Length;

   --  Derive the calibration factor from an image of a known dimension
   function "/" (Left : Millimeters; Right : Length) return Mm_Per_Px;

   --  Reverse the direction of the factor
   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 is a generic child package of Vision_Units, so it can use Millimeters declared in the parent as is. The body just converts the arguments to Long_Float, calculates, and converts to the result type. The type conversions are confined to this body, and the code that uses the package never has to write them.

flowchart TB
        accTitle: Each instance of the generic package gets its own types
        accDescr: Shows that instantiating the generic package Vision_Units.Axis twice as X_Axis and Y_Axis creates separate types such as X_Axis.Length and Y_Axis.Length, while Millimeters is the single type of the parent package shared by both.
        G["Vision_Units.Axis (generic package)"] -->|"new"| X["X_Axis"]
        G -->|"new"| Y["Y_Axis"]
        X --> XL["X_Axis.Length and the other 3 types"]
        Y --> YL["Y_Axis.Length and the other 3 types"]
        P["Vision_Units.Millimeters"] -.->|"Shared by x and y"| XL
        P -.-> YL

Figure 5: Each instance gets its own position, length and factor types, and only the millimeter type is shared by x and y.

Only the following three relations are defined between positions and lengths. Subtracting a position from a position gives a length, and adding a length to or subtracting a length from a position gives a position. Among the inherited operators, addition, multiplication and division of positions, subtraction returning a position, and exponentiation are removed.

The unary - that flips the sign and abs are kept for positions too. Removing them would make it impossible to write a negative position such as -5.0 as a literal. When I tried it with GNAT 13.3.0, P : constant Position := -5.0; gave cannot call abstract operation "-". Addition and subtraction of lengths, millimeters and calibration factors are kept because the unit of the result does not change.

flowchart TB
        accTitle: Operations defined between positions and lengths
        accDescr: Shows that subtracting a position from a position gives a length, adding or subtracting a length to a position gives a position, multiplying a length by the calibration factor gives millimeters, and that adding positions and multiplying lengths were removed.
        P1["Pos − pos"] --> L["Length"]
        P2["Pos ± length"] --> P["Position"]
        L2["Length × mm/px"] --> M["Millimeters"]
        M2["mm × px/mm"] --> L3["Length"]
        N1["Pos + pos"] -.-> E["Removed (abstract)"]
        N2["Length × length"] -.-> E

Figure 6: Among positions, lengths and millimeters, only the operations whose result unit is determined are kept.

The error GNAT reports for each mix-up

To the five mix-ups in Figure 2 I added two more cases — computing a midpoint, and exponentiation plus position-returning subtraction — and turned each into a small program and compiled it. Every one of them was a compile error with GNAT 13.3.0. With GNAT 16.1.0 on GitHub Actions, the messages were identical down to the column numbers.

Multiplying two pixel lengths

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

The program called an operator removed with abstract, so it was reported as cannot call abstract operation. If you need an area, define an area type and a Length × Length → area operator separately.

Forgetting the calibration factor

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

Converting a position as if it were a length

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

Only a length can be multiplied by the calibration factor, so an expression that multiplies a position by it cannot be written.

Adding positions to find the midpoint

Because addition of positions is removed, writing the midpoint as (left + right) / 2.0 is also a compile error. Numerically this expression gives the right value, but if positions could be added together, expressions that treat a position and a length as the same kind of value could be written as well. With the types in this article, the midpoint is written as “left edge + half of the length”.

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

Multiplying a y-direction length by the x-direction factor

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

The instance at y_axis.ads:2 and instance at x_axis.ads:2 in the messages tell you which instance each type belongs to.

Confusing mm/px with 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

No Length × Px_Per_Mm operator is defined, so this expression cannot be written. A px/mm factor can only be used in Millimeters × Px_Per_Mm, which converts millimeters to pixels.

Exponentiation and subtraction returning a position

The types I wrote first removed only +, * and /, so other operators inherited from Long_Float remained. Besides the four arithmetic operations, a derived type also inherits exponentiation **, unary - and abs¹. With the first types, Width ** 2 returned px² still as a length type, and an expression that put Right_Edge - Left_Edge into a position variable also went through. The former is the same mistake as multiplying two pixel lengths, and the latter is the mistake of treating a length as a position.

If ** and subtraction returning a position are also removed with abstract, as in the package above, every one of the following expressions is a compile error.

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;              --  holds px² as px
   Wrong_Pos : constant Position    := Right_Edge - Left_Edge;  --  holds a length as a position
   Mm2       : constant Millimeters := Millimeters'(3.0) ** 2;  --  holds mm² as 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

Because subtraction returning a position is removed, the only operator available for Right_Edge - Left_Edge is the one returning a length, and the result cannot be put into a position variable. To avoid forgetting to remove an operator, list the operators each type inherits and check one by one whether the unit of the result is right.

flowchart TB
        accTitle: Mix-ups and the kinds of GNAT errors
        accDescr: Shows that multiplying two pixel lengths, adding positions and exponentiation become errors for calling an abstract operator, that forgetting the factor becomes a type mismatch error, and that converting a position, confusing x and y, and reversing the factor become errors for operand types that do not match the operator.
        A["px × px, position + position, **"] --> E1["cannot call abstract operation"]
        B["Forgetting the factor"] --> E2["expected type … found type"]
        C["Position conversion, x and y, factor direction"] --> E3["invalid operand types for operator"]

Figure 7: Calling a removed operator is reported as an abstract error, and an undefined combination as an operand type error.

Deriving the calibration factor from a gauge and converting a width

After separating the types, the calculation looks like this. It derives the calibration factor from an image of a 10 mm gauge, converts the width of a part to millimeters, and converts 0.1 mm to pixels to widen the range in which to search for an edge.

with Ada.Text_IO;  use Ada.Text_IO;
with Vision_Units; use Vision_Units;
with X_Axis;       use X_Axis;

procedure Measure_Width is
   --  An image of a 10 mm gauge measured 500 px in the x direction
   Gauge_Mm : constant Millimeters := 10.0;
   Gauge_Px : constant X_Axis.Length := 500.0;
   Scale    : constant Mm_Per_Px := Gauge_Mm / Gauge_Px;

   --  Positions of the left and right edges of the part
   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;

   --  The midpoint is "left edge + half of the length"
   Center : constant Position := Left_Edge + Width_Px / 2.0;

   --  Convert 0.1 mm to px and widen the edge search range to the left
   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

If the types of the variables are written in their declarations, the operators on the right-hand side are chosen from the types. Gauge_Mm / Gauge_Px is Millimeters / Length, so the result is Mm_Per_Px. The abstract Length × Length is not a candidate in name resolution³, so 2.0 * Margin resolves uniquely to the Long_Float × Length operator.

flowchart TB
        accTitle: Deriving the calibration factor and then converting
        accDescr: Shows dividing the gauge millimeters by the gauge pixel length to get the mm/px factor, multiplying the part length by it to get millimeters, and multiplying millimeters by the reciprocal of the factor to get the pixel margin.
        G1["Gauge 10 mm"] --> S["mm/px factor"]
        G2["Gauge 500 px"] --> S
        S --> W["Width 510.5 px × factor = 10.21 mm"]
        S -->|"Invert"| I["px/mm factor"]
        I --> R["0.1 mm × px/mm = margin (px)"]

Figure 8: The factor is derived from a known dimension; mm/px is used from pixels to millimeters and px/mm in the other direction.

Do not compare tolerances as floating-point numbers

Even with the conversions protected by types, the pass/fail decision brings a different problem. Consider a drawing dimension of 5.00 ± 0.10 mm where a value of exactly 5.10 mm, the upper limit, is a pass. Measuring 510 px with a factor of 0.01 mm/px gives exactly 5.10 mm on paper. The measurement was calculated in the same Millimeters type as in the previous sections and compared with the upper limit as a 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

   --  The drawing is 5.00 ± 0.10 mm. Exactly 5.10 mm, the upper limit, is a pass
   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 comparison       : " & Boolean'Image (Long_Float (Measured) <= Upper));
      Put_Line ("Comparison after Mm rounding: "
                & Boolean'Image (Accept_Rounded (Measured, Drawing)));
   end Judge;

   --  Type conversion truncates, 'Round rounds to nearest
   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 comparison       : FALSE
Comparison after Mm rounding: TRUE
Mm (X)       = 5.099
Mm'Round (X) = 5.100

Neither 0.01 nor 5.1 can be represented exactly in binary floating point, so the measurement became 5.10000000000000053 and the upper limit 5.09999999999999964. A part exactly at the upper limit is rejected by the Long_Float comparison.

The measurement and the upper limit are calculated from the arguments of Judge because writing them with constants only, as in 510.0 * 0.01, would hide the error. Static expressions in Ada are evaluated exactly at compile time and rounded only once at the end⁶. So, as in an actual inspection, the calculation uses values passed at run time.

flowchart TB
        accTitle: The decision when comparing as floating-point numbers
        accDescr: Shows that the measurement of 510 pixels times 0.01 becomes 5.10000000000000053 and the upper limit of 5.00 plus 0.10 becomes 5.09999999999999964, so comparing them directly rejects a part exactly at the upper limit, while rounding to a 0.001 millimeter step makes it a pass.
        A["510 px × 0.01 mm/px"] --> M["5.10000000000000053"]
        B["5.00 mm + 0.10 mm"] --> U["5.09999999999999964"]
        M --> C{"Compare as Long_Float"}
        U --> C
        C --> NG["Fail"]
        M --> R["Round to a 0.001 mm step"]
        R --> OK["Pass at 5.100 mm"]

Figure 9: Comparing a measurement exactly at the upper limit as a floating-point number exceeds the limit; rounding to the drawing’s decimal places makes it a pass.

Matching the drawing’s decimal places with a decimal fixed-point type

For the decision I used a decimal fixed-point type that holds values at the drawing’s decimal places. type Mm is delta 0.001 digits 7; is a type with a 0.001 mm step and 7 digits, that is, -9999.999 to 9999.999 mm. In a decimal fixed-point type the step of the values (small) is equal to delta, and delta is restricted to a power of ten⁷. Values such as 0.100 and 5.100 are integer multiples of the step, so they are represented without error.

with Vision_Units;

package Tolerance is

   --  Decimal fixed-point type with a 0.001 mm step (-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;

   --  Pass including the lower and upper limits
   function Accept_Fixed (Measured : Mm; S : Spec) return Boolean is
     (Measured in S.Nominal - S.Minus .. S.Nominal + S.Plus);

   --  Round the measurement in millimeters to the drawing's decimal places before judging
   function Accept_Rounded (Measured : Vision_Units.Millimeters; S : Spec) return Boolean is
     (Accept_Fixed (Mm'Round (Measured), S));

end Tolerance;

When converting a floating-point measurement to Mm, mind the difference between a type conversion and 'Round. A type conversion to a decimal fixed-point type truncates toward zero if the value is not a multiple of the step⁸. 'Round rounds to the nearest multiple of the step and, when exactly halfway, picks the one farther from zero⁹. In the output of the previous section, 5.0996 became 5.099 with a type conversion and 5.100 with Mm'Round. The 5.10000000000000053 in the example above also became 5.100 with Mm'Round and was judged a pass.

Because the value is rounded before the comparison, a decision against an upper limit of 5.100 mm passes measurements up to just below 5.1005 mm. This is a deliberate policy: values up to half a step beyond the limit still pass. Decide in advance whether this is acceptable for the drawing tolerance. Also, Mm'Round raises Constraint_Error if the result falls outside the range of Mm (±9999.999).

The parameter type of Accept_Rounded is Millimeters. If the parameter were Long_Float, passing a typed value would require a Long_Float (…) type conversion, and a pixel length could be passed in exactly the same way. With a Millimeters parameter, a call that passes a pixel length was a compile error with expected type "Millimeters". 'Round can also be applied to a Millimeters value as it is.

flowchart TB
        accTitle: Type conversion to a decimal fixed-point type and 'Round
        accDescr: Shows that when converting the floating-point value 5.0996 to the decimal fixed-point type Mm, a type conversion truncates toward zero to 5.099, while 'Round rounds to the nearest multiple to 5.100.
        X["5.0996 (Long_Float)"] -->|"Mm (X)"| T["5.099 (truncated toward 0)"]
        X -->|"Mm'Round (X)"| R["5.100 (nearest multiple)"]

Figure 10: A type conversion to a decimal fixed-point type truncates, and ‘Round rounds to nearest.

For an ordinary, non-decimal fixed-point type, if you write only delta, the implementation chooses the step from the powers of two not greater than delta⁷. Specifying Small makes the step 0.001.

with Ada.Text_IO; use Ada.Text_IO;

procedure Small_Check is
   --  With only delta written, small is a power of two not greater than delta
   type Mm_Binary is delta 0.001 range -1000.0 .. 1000.0;

   --  Specifying small lets multiples of 0.001 be represented exactly
   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

Both GNAT 13.3.0 and 16.1.0 made the step of Mm_Binary 2⁻¹⁰ (0.0009765625), and 0.1 became 0.099609375. Compiling with -gnatwa, which enables all warnings (or -gnatwb), gives a warning that 0.1 is not a multiple of the step. With the default switches no warning is given. If you want to hold drawing values exactly, use a decimal fixed-point type or specify Small.

flowchart TB
        accTitle: How the step of a fixed-point type is determined
        accDescr: Shows that a decimal fixed-point type has a step equal to delta, a power of ten, that an ordinary fixed-point type with only delta written gets a power-of-two step and cannot represent 0.1 exactly, and that specifying Small makes the step 0.001.
        D["delta 0.001 digits 7 (decimal)"] --> D1["Step 0.001"]
        O["delta 0.001 range … (ordinary)"] --> O1["Step 2⁻¹⁰ (GNAT 13 and 16)"]
        O1 --> O2["0.1 becomes 0.099609375"]
        S["Ordinary type + Small => 0.001"] --> S1["Step 0.001"]

Figure 11: To hold values at the drawing’s decimal places, use a decimal fixed-point type or a fixed-point type with Small specified.

I split the work so that everything up to the conversion is calculated in types derived from Long_Float, and the value is brought to the drawing’s decimal places with Mm'Round just before the decision. Fine-grained values such as sub-pixel edge positions are calculated in floating point, and only the comparison that decides pass or fail is done in fixed point.

Checking dimensions with GNAT’s dimension system

GNAT has its own mechanism for giving floating-point types dimensions. If you declare the base dimensions of a type with the Dimension_System aspect and give a subtype a combination of dimensions with the Dimension aspect, an expression whose dimensions do not match is a compile error¹⁰¹¹. This feature is not in the Ada standard, so it cannot be used with compilers other than GNAT. GNAT also provides System.Dim.Mks, built from the seven SI base units.

For dimensional inspection, I made a type whose base dimensions are millimeters and pixels in the x and y directions.

package Vision_Dims is

   --  A GNAT-specific aspect. Make mm and x/y pixels the base dimensions
   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

Output through System.Dim.Float_IO puts the dimension symbol after the value. Expressions whose dimensions do not match were reported as follows.

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;                    --  forgot the factor
   Mixed   : constant Mm_Length := Height * Scale_X;         --  x and y
   Inverse : constant Mm_Length := Width * (1.0 / Scale_X);  --  factor direction
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]

All four mix-ups were reported as dimension mismatches. [L] is the dimension of millimeters, and [X] and [Y] are the dimensions of pixels in the x and y directions.

In the dimension system, the compiler calculates the dimensions of the results of multiplication and division. px × px is not forbidden; it is treated as a value of dimension [X**2], so it can also be used as an area. mm/px and px/mm are distinguished by the sign of the exponent of the dimension. There is no need to define operators one by one.

On the other hand, the dimension system cannot distinguish positions from lengths, because both have the dimension [X].

flowchart TB
        accTitle: Mix-ups prevented by defining operators and by the dimension system
        accDescr: Shows that the method of derived types and defined operators prevents px×px, forgetting the factor, converting a position, confusing x and y, and reversing the factor; that GNAT's dimension system prevents all mix-ups except converting a position; and that an area can be calculated with the dimension X**2.
        T["Derived types + defined operators"] --> T1["Prevents the 5 mix-ups"]
        T1 --> T2["Operators written one by one"]
        D["GNAT's dimension system"] --> D1["Prevents 4, all except position conversion"]
        D1 --> D2["Area can be calculated as X**2"]
        D2 --> D3["Usable only with GNAT"]

Figure 12: The dimension system checks dimensions without writing operators, but it cannot distinguish positions from lengths and cannot be used outside GNAT.

If you want to distinguish positions from lengths, or to build with compilers other than GNAT, choose the method of derived types and operators from the first half.

Proving with SPARK that the conversion result stays within the type’s range

Even with the units aligned by types, whether a value fits in the range of its type is a separate question. The types in the first half are derived from Long_Float, so no range is specified for them. I wrote the conversion with fixed-point types that have ranges and proved with SPARK’s GNATprove that the range checks cannot fail. SPARK is a subset of Ada, and GNATprove is a tool that proves properties of code written in SPARK. See Introduction to Formal Verification with SPARK for details.

package Scaled_Length with SPARK_Mode is

   --  Length with a 0.01 px step. Image widths up to 16384 px
   type Px_Length is delta 0.01 range 0.0 .. 16_384.0
     with Small => 0.01;

   --  Calibration factor with a 0.00001 mm/px step
   type Mm_Per_Px is delta 0.000_01 range 0.000_01 .. 1.0
     with Small => 0.000_01;

   --  Length with a 0.001 mm step
   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;

The product of two fixed-point values has the type universal_fixed, and the type of the result is determined by the context or a type conversion¹². Here the type conversion Mm (L * S) makes it explicit, and a range check is performed on the conversion to Mm. The length is at most 16384 px and the factor at most 1.0 mm/px, so the product is at most 16384 mm, which fits in the range of Mm.

Running GNATprove with --level=2 --report=all --checks-as-errors=on¹³ proved three checks: the overflow check of L * S, the range check of the conversion to Mm, and that To_Mm always terminates.

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

What this proof shows is only that the result fits in the range of Mm; it says nothing about how the value is rounded. For a type conversion to a non-decimal fixed-point type, the standard only specifies that the result is a value within the accuracy of the target type⁸. With GNAT 13.3.0 on my machine it truncated: 0.19 px × 0.01 mm/px (0.0019 mm) became 0.001 mm, and 510.55 px × 0.01999 mm/px (10.2058945 mm) became 10.205 mm. The result can be up to 0.001 mm too small, so if you use it for decision, decide the rounding in advance as in the previous section.

Next I prepared a package that widens the upper limit of the image width to 1000000 px. The only difference is the range of Px_Length.

   --  When the upper limit of the image width is widened to 1000000 px
   type Px_Length is delta 0.01 range 0.0 .. 1_000_000.0
     with Small => 0.01;

In this package the product can reach 1000000 mm and exceed the range of Mm. GNATprove could not prove the range check and reported that it “might fail” with high severity.

 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

The e.g. line is an example of values for which the check fails. With L = 1000000 px and S = 0.10001 mm/px, the product is 100010 mm, which exceeds the upper limit of Mm. The possible fix line shows a way to fix it by narrowing the ranges of L and S in the precondition of To_Mm. Because --checks-as-errors=on was given, GNATprove exited with code 1 when unproved checks remained.

In a normal build without GNATprove, this mistake is found only at run time. When I tried the widened package with a small program (not shown in this article) that calls To_Mm with a length and a factor given as arguments, it returned a value for 16384 px and stopped with Constraint_Error for 1000000 px.

$ ./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: Proving the conversion result from the type ranges
        accDescr: Shows that the upper limit of the product, 16384 millimeters, follows from the length limit of 16384 pixels and the factor limit of 1.0, so it fits in the range of Mm and can be proved, while widening the length limit to 1000000 pixels makes the product exceed the range of Mm so it cannot be proved, and at run time it becomes Constraint_Error.
        A["Length ≤ 16384, factor ≤ 1.0"] --> B["Product ≤ 16384 mm"]
        B --> C["Within the range of Mm, so it can be proved"]
        W["Length limit widened to 1000000"] --> X["Product ≤ 1000000 mm"]
        X --> Y["Exceeds the range of Mm, cannot be proved"]
        Y -.-> Z["Constraint_Error at run time"]

Figure 13: GNATprove derives the range of the product from the type ranges and reports it if the result may not fit in the target type.

The same idea in C# and F#

In C# you can make pixel lengths and millimeters separate types such as readonly record struct and define only the meaningful operators¹⁴. A newly created struct has no arithmetic operators, so there is no step of removing inherited operators as in Ada. It should be possible to generate the x and y types from a single definition by passing a marker type for the axis as a generic type argument, but I did not try that for this article. For comparisons at the drawing’s decimal places, the decimal type, a decimal floating-point number, can be used¹⁵. F# has units of measure as a language feature and can check combinations of units much like GNAT’s dimension system¹⁶.

What types cannot prevent

Types check only the kinds of values and the combinations of operations. The following mistakes remain even with separate types.

• Errors in the value of the calibration factor itself, such as a mistyped gauge dimension or a gauge placed in the wrong position in the image.
• Cases where a single factor cannot do the conversion because of lens distortion or shooting at an angle. If the factor varies with the location in the image, a separate correction that derives the factor from the position is needed.
• Boundaries with external libraries. Where the double returned by an edge detection library is converted to a Position, a person decides which axis the position belongs to. Keep these type conversions in one place and make that code a review target.
• Untyped literals. A numeric literal such as 2.0 takes whatever type lets the expression resolve. In Width_Px * 2.0, 2.0 became a mm/px factor, and in Millimeters'(1.0) * 50.0, 50.0 became a px/mm factor. Writing the value of an x-direction factor as a literal for a y-direction length also goes through as a y factor. All of these compiled without warnings with -gnatwa. Make factors named, typed constants and do not write literal factors directly in expressions.

flowchart TB
        accTitle: What types can and cannot prevent
        accDescr: Shows that types prevent errors in the kinds of values and the combinations of operations, but cannot prevent errors in the value of the calibration factor, changes in the factor due to lens distortion, axis mix-ups where values from external libraries are received, or factors written as untyped literals.
        T["Type checking"] --> OK["Kinds of values and combinations of operations"]
        T -.-> NG["Cannot be checked by types"]
        NG -.-> N1["Wrong factor value"]
        NG -.-> N2["Location-dependent factors"]
        NG -.-> N3["Boundary conversion"]
        NG -.-> N4["Untyped literal factors"]

Figure 14: Types check the combinations of operations, but people must confirm the correctness of the values and the decisions at the places where values come in from outside.

Test environment and what was not verified

• Compilation, execution and error messages were confirmed on November 10, 2026 with GNAT 13.3.0 (the Ubuntu package) and gprbuild on my own Ubuntu 24.04 machine. The compiler switches were -gnat2022 -gnatwa. On a GitHub Actions Ubuntu 24.04 runner, I also built and ran the same code with GNAT 16.1.0 installed by Alire 2.1.1 and confirmed that the error messages and outputs were the same. With other versions of GNAT, the wording of messages and the column numbers may differ.
• The step of Mm_Binary being 2⁻¹⁰ is the result with GNAT 13.3.0 and 16.1.0. The standard only specifies “a power of two not greater than delta”.
• The GNATprove proofs were done on a GitHub Actions Ubuntu 24.04 runner with GNATprove FSF 16.1.0 (Why3 1.8.2+git, Alt-Ergo 2.6.1, cvc5 1.3.2, Z3 4.15.4) at --level=2. GNATprove is not installed with GNAT 13.3.0 on my machine.
• Images from a real camera, the combination with an edge detection library, and building on Windows were not tried.
• The complete project used for verification is not published; the code in this article is an excerpt from it.

Related Articles

This article is part of the series “Ada and Machine Vision”. The other articles in the series are:

• Proving Image Processing Free of Out-of-Bounds Access with SPARK — Binarization, Smoothing, Labeling and a Speed Comparison with C
• Receiving GigE Vision Packets with Ada Types — Pitfalls of Representation Clauses and a SPARK-Proved Parser
• Frame Acquisition Without Drops Using Ada Tasks — A Protected-Object Ring Buffer and Priorities
• Calling Ada Inspection Logic from a C# Inspection App — Passing Image Buffers Without Copying and Guarding the Boundary

Related existing articles:

• The Appeal of the Ada Language — Expressing Design Through Types and Powering Software That Runs for Decades
• Generic Programming in Ada — Contracts, Types, and Zero-Cost Reuse
• Introduction to Formal Verification with SPARK — From Ada Contracts to Mathematical Proof
• Dropped Frames with GigE Vision and USB3 Vision Cameras — Locating the Cause and the Windows Settings to Review

References

Related Articles

Recent articles sharing the same tags. Deepen your understanding with closely related topics.

Related Topics

These are topic pages close to this theme. Starting from the article, you can go on to related services and other articles.

Services Connected to This Topic

This article leads to the following service pages. Start from the entry point closest to your situation.

Frequently Asked Questions

Questions commonly asked at the time of consultation about the topic of this article.

If pixels and millimeters are separate types in Ada, are all unit mix-ups prevented?

Making them derived types is not enough. A derived type inherits the operators of its parent type, so multiplying two pixel lengths returns a pixel length. Redeclare the meaningless operators as abstract so that they cannot be called, and define only the meaningful operators, such as length × calibration factor → millimeters.

Can types also prevent mixing up the x and y calibration factors?

Yes. Declare the position, length and calibration factor types inside a generic package and instantiate it twice, once for x and once for y; each instance then has its own types. An expression that multiplies a y-direction length by an x-direction factor was a compile error with GNAT.

What goes wrong when tolerance checks are done with floating-point numbers?

A value exactly at the upper limit can be rejected. Measuring 510 px at 0.01 mm/px gives 5.10000000000000053 when computed in Long_Float, which exceeded the 5.10 mm upper limit. Rounding the measurement to a decimal fixed-point type with a 0.001 mm step before comparing lets it be judged as a pass.

Author Profile

Profile page for the article author.

Go Komura

Representative of KomuraSoft LLC

Focused on Windows software development, technical consulting, and bug investigation, with particular strength in projects where existing assets remain and in investigating failures whose cause is hard to see.