Performing Dimensionality Analysis in GNAT (GNAT User’s Guide for Native Platforms)

6.5 Performing Dimensionality Analysis in GNAT ¶

The GNAT compiler supports dimensionality checking. The user can specify physical units for objects, and the compiler will verify that uses of these objects are compatible with their dimensions, in a fashion that is familiar to engineering practice. The dimensions of algebraic expressions (including powers with static exponents) are computed from their constituents.

This feature depends on Ada 2012 aspect specifications, and is available from version 7.0.1 of GNAT onwards. The GNAT-specific aspect Dimension_System allows you to define a system of units; the aspect Dimension then allows the user to declare dimensioned quantities within a given system. (These aspects are described in the `Implementation Defined Aspects' chapter of the `GNAT Reference Manual').

The major advantage of this model is that it does not require the declaration of multiple operators for all possible combinations of types: it is only necessary to use the proper subtypes in object declarations.

The simplest way to impose dimensionality checking on a computation is to make use of one of the instantiations of the package System.Dim.Generic_Mks, which are part of the GNAT library. This generic package defines a floating-point type MKS_Type, for which a sequence of dimension names are specified, together with their conventional abbreviations. The following should be read together with the full specification of the package, in file s-digemk.ads.

type Mks_Type is new Float_Type
  with
   Dimension_System => (
     (Unit_Name => Meter,    Unit_Symbol => 'm',   Dim_Symbol => 'L'),
     (Unit_Name => Kilogram, Unit_Symbol => "kg",  Dim_Symbol => 'M'),
     (Unit_Name => Second,   Unit_Symbol => 's',   Dim_Symbol => 'T'),
     (Unit_Name => Ampere,   Unit_Symbol => 'A',   Dim_Symbol => 'I'),
     (Unit_Name => Kelvin,   Unit_Symbol => 'K',   Dim_Symbol => "Theta"),
     (Unit_Name => Mole,     Unit_Symbol => "mol", Dim_Symbol => 'N'),
     (Unit_Name => Candela,  Unit_Symbol => "cd",  Dim_Symbol => 'J'));

The package then defines a series of subtypes that correspond to these conventional units. For example:

subtype Length is Mks_Type
  with
   Dimension => (Symbol => 'm', Meter  => 1, others => 0);

and similarly for Mass, Time, Electric_Current, Thermodynamic_Temperature, Amount_Of_Substance, and Luminous_Intensity (the standard set of units of the SI system).

The package also defines conventional names for values of each unit, for example:

m   : constant Length           := 1.0;
kg  : constant Mass             := 1.0;
s   : constant Time             := 1.0;
A   : constant Electric_Current := 1.0;

as well as useful multiples of these units:

 cm  : constant Length := 1.0E-02;
 g   : constant Mass   := 1.0E-03;
 min : constant Time   := 60.0;
 day : constant Time   := 60.0 * 24.0 * min;
...

There are three instantiations of System.Dim.Generic_Mks defined in the GNAT library:

System.Dim.Float_Mks based on Float defined in s-diflmk.ads.
System.Dim.Long_Mks based on Long_Float defined in s-dilomk.ads.
System.Dim.Mks based on Long_Long_Float defined in s-dimmks.ads.

Using one of these packages, you can then define a derived unit by providing the aspect that specifies its dimensions within the MKS system, as well as the string to be used for output of a value of that unit:

subtype Acceleration is Mks_Type
  with Dimension => ("m/sec^2",
                     Meter => 1,
                     Second => -2,
                     others => 0);

Here is a complete example of use:

with System.Dim.MKS; use System.Dim.Mks;
with System.Dim.Mks_IO; use System.Dim.Mks_IO;
with Text_IO; use Text_IO;
procedure Free_Fall is
  subtype Acceleration is Mks_Type
    with Dimension => ("m/sec^2", 1, 0, -2, others => 0);
  G : constant acceleration := 9.81 * m / (s ** 2);
  T : Time := 10.0*s;
  Distance : Length;

begin
  Put ("Gravitational constant: ");
  Put (G, Aft => 2, Exp => 0); Put_Line ("");
  Distance := 0.5 * G * T ** 2;
  Put ("distance travelled in 10 seconds of free fall ");
  Put (Distance, Aft => 2, Exp => 0);
  Put_Line ("");
end Free_Fall;

Execution of this program yields:

Gravitational constant:  9.81 m/sec^2
distance travelled in 10 seconds of free fall 490.50 m

However, incorrect assignments such as:

Distance := 5.0;
Distance := 5.0 * kg;

are rejected with the following diagnoses:

Distance := 5.0;
   >>> dimensions mismatch in assignment
   >>> left-hand side has dimension [L]
   >>> right-hand side is dimensionless

Distance := 5.0 * kg:
   >>> dimensions mismatch in assignment
   >>> left-hand side has dimension [L]
   >>> right-hand side has dimension [M]

The dimensions of an expression are properly displayed, even if there is no explicit subtype for it. If we add to the program:

Put ("Final velocity: ");
Put (G * T, Aft =>2, Exp =>0);
Put_Line ("");

then the output includes:

Final velocity: 98.10 m.s**(-1)

The type Mks_Type is said to be a `dimensionable type' since it has a Dimension_System aspect, and the subtypes Length, Mass, etc., are said to be `dimensioned subtypes' since each one has a Dimension aspect.

The Dimension aspect of a dimensioned subtype S defines a mapping from the base type’s Unit_Names to integer (or, more generally, rational) values. This mapping is the `dimension vector' (also referred to as the `dimensionality') for that subtype, denoted by DV(S), and thus for each object of that subtype. Intuitively, the value specified for each Unit_Name is the exponent associated with that unit; a zero value means that the unit is not used. For example:

declare
   Acc : Acceleration;
   ...
begin
   ...
end;

Here DV(Acc) = DV(Acceleration) = (Meter=>1, Kilogram=>0, Second=>-2, Ampere=>0, Kelvin=>0, Mole=>0, Candela=>0). Symbolically, we can express this as Meter / Second**2.

The dimension vector of an arithmetic expression is synthesized from the dimension vectors of its components, with compile-time dimensionality checks that help prevent mismatches such as using an Acceleration where a Length is required.

The dimension vector of the result of an arithmetic expression `expr', or DV(`expr'), is defined as follows, assuming conventional mathematical definitions for the vector operations that are used:

If `expr' is of the type `universal_real', or is not of a dimensioned subtype, then `expr' is dimensionless; DV(`expr') is the empty vector.
DV(`op expr'), where `op' is a unary operator, is DV(`expr')
DV(`expr1 op expr2') where `op' is “+” or “-” is DV(`expr1') provided that DV(`expr1') = DV(`expr2'). If this condition is not met then the construct is illegal.
DV(`expr1' * `expr2') is DV(`expr1') + DV(`expr2'), and DV(`expr1' / `expr2') = DV(`expr1') - DV(`expr2'). In this context if one of the `expr's is dimensionless then its empty dimension vector is treated as (others => 0).
DV(`expr' ** `power') is `power' * DV(`expr'), provided that `power' is a static rational value. If this condition is not met then the construct is illegal.

Note that, by the above rules, it is illegal to use binary “+” or “-” to combine a dimensioned and dimensionless value. Thus an expression such as acc-10.0 is illegal, where acc is an object of subtype Acceleration.

The dimensionality checks for relationals use the same rules as for “+” and “-“, except when comparing to a literal; thus

acc > len

is equivalent to

acc-len > 0.0

and is thus illegal, but

acc > 10.0

is accepted with a warning. Analogously a conditional expression requires the same dimension vector for each branch (with no exception for literals).

The dimension vector of a type conversion T(`expr') is defined as follows, based on the nature of T:

If T is a dimensioned subtype then DV(T(`expr')) is DV(T) provided that either `expr' is dimensionless or DV(T) = DV(`expr'). The conversion is illegal if `expr' is dimensioned and DV(`expr') /= DV(T). Note that vector equality does not require that the corresponding Unit_Names be the same.
As a consequence of the above rule, it is possible to convert between different dimension systems that follow the same international system of units, with the seven physical components given in the standard order (length, mass, time, etc.). Thus a length in meters can be converted to a length in inches (with a suitable conversion factor) but cannot be converted, for example, to a mass in pounds.
If T is the base type for `expr' (and the dimensionless root type of the dimension system), then DV(T(`expr')) is DV(expr). Thus, if `expr' is of a dimensioned subtype of T, the conversion may be regarded as a “view conversion” that preserves dimensionality.
This rule makes it possible to write generic code that can be instantiated with compatible dimensioned subtypes. The generic unit will contain conversions that will consequently be present in instantiations, but conversions to the base type will preserve dimensionality and make it possible to write generic code that is correct with respect to dimensionality.
Otherwise (i.e., T is neither a dimensioned subtype nor a dimensionable base type), DV(T(`expr')) is the empty vector. Thus a dimensioned value can be explicitly converted to a non-dimensioned subtype, which of course then escapes dimensionality analysis.

The dimension vector for a type qualification T'(`expr') is the same as for the type conversion T(`expr').

An assignment statement

Source := Target;

requires DV(Source) = DV(Target), and analogously for parameter passing (the dimension vector for the actual parameter must be equal to the dimension vector for the formal parameter).