![[Ada Information Clearinghouse]](small_adaic_logo.gif){kind=logo}
Data type definitions are performed in two steps:
Furthermore, to establish the correctness of a program that uses a given formulation of data and a given representation, we have two disjoint proofs. First we show that the program is correct given the formulation of the data types and algorithms. Then we show that the chosen representation is a correct implementation of the data. The separation also ensures that users do not make implicit assumptions about the representation of data.
If at a later stage a different representation is selected, for example to reduce storage space, the formulation of the algorithms need not be modified. Conversely, if the algorithms of a program are modified, the representation need not be affected.
Another advantage is textual simplicity. In some cases, the representation of a data type is dictated by external considerations such as the form of a hardware interface: the description of the representation may then be correspondingly complex. However, by keeping the logical description textually distinct from that of the representation we can retain the simplicity of the logical description.
The above separation principle is reflected in Ada by a clear textual separation between the declaration of the logical properties of data and the specification of the properties of their representation. Properties of the representation are specified by representation clauses. These clauses are optional, and distinct from the declaration of the logical properties. The parts of a program that are hardware- specific are thus easy to identify.