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
allows you to define a system of units; the aspect
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
are part of the GNAT library. This generic package defines a floating-point
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
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
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
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)
Mks_Type is said to be a `dimensionable type' since it has a
Dimension_System aspect, and the subtypes
are said to be `dimensioned subtypes' since each one has a
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;
(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:
DV(`expr')is the empty vector.
DV(`op expr'), where `op' is a unary operator, is
DV(`expr1 op expr2')where `op' is "+" or "-" is
DV(`expr2'). If this condition is not met then the construct is illegal.
DV(`expr1' * `expr2')is
DV(`expr1' / `expr2')=
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
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
Tis a dimensioned subtype then
DV(T)provided that either `expr' is dimensionless or
DV(`expr'). The conversion is illegal if `expr' is dimensioned and
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.
Tis the base type for `expr' (and the dimensionless root type of the dimension system), then
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.
Tis 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
An assignment statement
Source := Target;
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).