Gem #136: How tall is a kilogram?
by Vincent Pucci —AdaCore
Let's get started...
This Gem outlines the new GNAT dimensionality checking system. This feature relies on Ada 2012 aspect specifications, and is available from version 7.0.1 of GNAT onwards.
The GNAT compiler now supports dimensionality checking. Ever since the appearance of user-defined operators in Ada 83 there have been attempts to use these to declare types with dimensions, and perform dimensionality checks on scientific code. These attempts were unfortunately unwieldy and were not adopted by the language. The system we describe here is lightweight and relies on the aspect specifications introduced in Ada 2012. We hope that the engineering and scientific community will find it convenient and easy to use.
Before exploring the implementation of this feature, let's first consider a common example in physics: the free fall problem. We want to evaluate the distance traveled by a body in 10 seconds of free fall knowing the gravitational acceleration on Earth. The well-known solution is:
distance = 1/2 * g * t**2 where t = 10s.
A question arises here : how do we define dimensioned objects in Ada?
For this purpose, The GNAT compiler provides the International System of Units, i.e., the meter-kilogram-second (MKS) system of units, in package System.Dim.Mks. GNAT also provides output facilities for this system of units in package System.Dim.Mks_IO.
The package System.Dim.Mks defines a numeric base type Mks_Type, and subtypes of it that correspond to physical quantities (such as Length, Time) as well as constants of each dimensioned quantity (such as m, s) are defined.
Using these two packages, we are now able to convert our free fall problem into Ada code:
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
G : constant Mks_Type := 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 traveled in 10 seconds of free fall: ");
Put (Distance, Aft => 2, Exp => 0);
Put_Line ("");
end Free_Fall;
Compiling and running our example yields:
$ gnatmake -q -gnat2012 free_fall.adb $ ./free_Fall
Gravitational constant: 9.81 m.s**(-2) distance traveled in 10 seconds of free fall: 490.50 m
The properties of type Mks_Type and its subtypes Time and Length are defined by means of two new GNAT-specific aspects:
The aspect Dimension_System allows the user to define a system of units. The aspect Dimension_System can only apply to a numeric type, typically a floating point type of the appropriate precision (any numeric type can be used as a base). A type (more accurately a first subtype) to which the aspect Dimension_System applies is a dimensioned type. The syntax of an aspect Dimension_System is as follows:
with Dimension_System => ( DIMENSION {, DIMENSION});
DIMENSION ::= ( [Unit_Name =>] IDENTIFIER, [Unit_Symbol =>] SYMBOL, [Dim_Symbol =>] SYMBOL)
SYMBOL ::= STRING_LITERAL | CHARACTER_LITERAL
That is to say, the value of the aspect is an aggregate. Up to 7 dimensions (corresponding to the International System of Units) can be specified.
The aspect Dimension allows the user to declare dimensioned quantities within a given system. An aspect Dimension applies only to a subtype of a dimensioned type. A subtype to which the aspect Dimension applies is a dimensioned subtype. The syntax of an aspect Dimension is as follows:
with Dimension => ( [[Symbol =>] SYMBOL,] DIMENSION_VALUE {, DIMENSION_VALUE});
SYMBOL ::= STRING_LITERAL | CHARACTER_LITERAL
DIMENSION_VALUE ::= RATIONAL | others => RATIONAL | DISCRETE_CHOICE_LIST => RATIONAL
RATIONAL ::= [-] NUMERAL [/NUMERAL]
Using both aspects, users are thus able to define their own systems of units and to compute dimensioned formulae. The compiler will diagnose dimension mismatch in computations and assignments.
Now, let's have a closer look at the MKS package. The MKS dimensioned type is defined as follows:
type Mks_Type is new Long_Long_Float
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'));
A dimensioned subtype (such as Length, Mass, Time, Electric_Current, Thermodynamic_Temperature, Amount_Of_Substance, Luminous_Intensity) is defined as follows:
subtype Length is Mks_Type
with Dimension => (Symbol => 'm',
Meter => 1,
others => 0);
The package also defines conventional names for values of each unit such as:
m : constant Length := 1.0; cm : constant Length := 1.0E-02;
In both Dimension and Dimension_System aspects, symbols passed as arguments are used for output purposes. Indeed, GNAT also provides dimension-specific output facilities in two generic packages for both integer- and float-dimensioned types: System.Dim.Integer_IO. and System.Dim.Float_IO. The Put routines defined in these packages output the numeric value, followed by the dimension vector of the item passed as parameter (System.Dim.Mks_IO, used in the free fall example, is an instance of System.Dim.Float_IO instantiated with the Mks_Type in package System.Dim.Mks).
Back to the free fall example, the careful reader will have noticed that the gravitational constant G could be defined by introducing a new dimensioned subtype:
subtype Acceleration is Mks_Type
with Dimension => ("m/sec^2
Meter => 1,
Second => -2,
others => 0);
G : constant Acceleration := 9.81 * m / (s**2);
The execution of the free_fall program now yields:
$ ./free_fall
Gravitational constant: 9.81 m/sec^2 distance traveled in 10 seconds of free fall: 490.50 m
The purpose of dimensional analysis is to verify dimension consistency within physical relations, and prevent the kind of errors that have become legendary, such as the space probe that was lost because one module computed in metric units and another one in Imperial units. GNAT checks dimension consistency on assigments, parameter passing, addition operations, and comparisons. GNAT computes the resulting dimensions of multiplication and exponentiation operations.
For instance, in the free fall example, an incorrect assignment such as:
Distance := 5.0 * kg;
is rejected at compile time with the following diagnoses:
$ ./free_fall
free_fall.adb:15:13: dimensions mismatch in assignment
free_fall.adb:15:13: left-hand side has dimension [L]
free_fall.adb:15:13: right-hand side has dimension [M]
Incorrect arithmetic operations also lead to such diagnoses. For example, in the free fall program:
Distance := T + G;
is rejected as follows: $ ./free_fall
free_fall.adb:15:18: both operands for operation "+" must have same dimensions
free_fall.adb:15:18: left operand has dimension [T]
free_fall.adb:15:18: right operand has dimension [L.T**(-2)]
This introduction should be sufficient for the user to start experimenting with the existing packages on engineering/scientific code. The next step for the ambitious reader is to create a new system of units, such as the centimeter-gram-second (CGS) system, and test as many physical formulae as possible in order to get familiarized with this new feature. If multiple systems are present, it will be natural to introduce conversion routines between them. Because the base types of different systems are distinct, type checking ensures that these values cannot be accidentally mixed in the same computation.
This is a new feature of the GNAT tool chain. We welcome comments from users, suggestions for improvements, and interesting examples of use!