![[Ada Information Clearinghouse]](small_adaic_logo.gif){kind=logo}
Although the details of the alternate representations are not part of the logical properties, we will show with the following example that the knowledge of the existence of alternate representations is, itself, a logical property.
procedure CONVERT is
-- declarations of the logical properties:
type DAY is (MON, TUE, WED, THU, FRI, SAT, SUN);
X, Y : DAY;
-- representation clauses (not in the Ada syntax):
representation FORM_A of DAY is
(MON => 0, TUE => 1, WED => 2,
THU => 3, FRI => 4, SAT => 5, SUN => 6);
representation FORM_B of DAY is
(MON => 1, TUE => 2, WED => 3,
THU => 4, FRI => 5, SAT => 6, SUN => 7);
for X use representation FORM_A;
for Y use representation FORM_B;
-- end of representation clauses (in hypothetical syntax)
begin
...
Y := X;
...
end CONVERT;
|
In trying to establish the correctness of the above procedure, one finds that the information contained in the logical declarations of X and Y does not suffice. It can only be concluded that X and Y are of type DAY. To complete the correctness proof (that conversion is properly effected) it is necessary to consider representation clauses, and hence to violate the separation principle mentioned earlier. We are thus led to the conclusion that any attempt to hide the existence of multiple representations at the logical level ultimately leads to a violation of the separation principle.
If we need two different representations, two different types are therefore required, although these two types should have identical logical properties: the solution to this problem is to use derived types. For example, a type B can be derived from a type A by declaring
type B is new A;
Since B derives its characteristics from A, both types have the same characteristics, for example the same components. However, they are distinct types and it is hence possible to specify different representations for A and for B. Change of representation can be achieved by explicit conversion between objects of types A and B since such conversions are defined for derived types. Derivation has the effect of creating a type with the same characteristics as another type, without rewriting its entire description (that would define a distinct type for which no conversions are possible).
The one type - one representation principle must be understood in terms of the knowledge that the user has from the existence (as opposed to the details) of a representation. It means that if a representation is explicitly specified for a type, then only one representation can be specified for this type. However, in cases where the representation is implicitly selected by the compiler, this does not preclude the use of different internal representations in different contexts - out of sight of the user.
Y := EXTERNAL_DAY(X);
in the conversion problem presented earlier. The full solution may be properly expressed in Ada as follows:
procedure CONVERT is
-- declaration of the logical properties:
type DAY is (MON, TUE, WED, THU, FRI, SAT, SUN);
type EXTERNAL_DAY is new DAY; -- a derived type
X : DAY := DAY'FIRST;
Y : EXTERNAL_DAY;
-- representation clauses for the two types:
for DAY use
(MON => 0, TUE => 1, WED => 2,
THU => 3, FRI => 4, SAT => 5, SUN => 6);
for EXTERNAL_DAY use
(MON => 1, TUE => 2, WED => 3,
THU => 4, FRI => 5, SAT => 6, SUN => 7);
-- end of representation clauses
begin
...
Y := EXTERNAL_DAY(X);
...
end CONVERT;
|
The correctness of this procedure can now be established without violation of the separation principle. First, we have to show that the program is correct given the definition of X and Y: Initially X contains a value of type DAY; the conversion EXTERNAL_DAY(X) is legal since the type EXTERNAL_DAY, is derived from the type DAY - it converts the value of X into a value of type EXTERNAL_DAY, which is finally assigned to Y. Secondly, it must be shown that the representations given for DAY and EXTERNAL_DAY are correct.
The same simple strategy would be used in the previously mentioned case of conversion of a record structure between a packed representation and an unpacked representation:
type OBJECT is
record
-- declaration of the components of objects
end record;
type EXTERNAL_OBJECT is new OBJECT; -- a distinct type derived from
OBJECT
for EXTERNAL_OBJECT use
record
...
-- definition of the layout of record components
end record;
X : OBJECT;
Y : EXTERNAL_OBJECT;
...
X := OBJECT(Y); -- unpack
...
Y := EXTERNAL_OBJECT(X); -- pack
|
type V(D : BOOLEAN := TRUE) is
record
case D is
when TRUE => I : INTEGER;
when FALSE => R : REAL;
end case;
end record;
type W is new V;
for V use ...
for W use ...
X : V;
Y : W;
...
X := V(Y);
|
The implementation of the above assignment cannot be achieved as simply as for a normal record assignment. It must be done on a field by field basis, which is equivalent to the following program (apart from the restriction on assignment to the discriminant):
X.D := Y.D; -- not legal Ada
case Y.D is
when TRUE => X.I := Y.I;
when FALSE => X.R := Y.R;
end case;
|
Producing such code is well within the capability of present compilation techniques. Nevertheless it is complex and can be somewhat costly on some computers (note that there might be variants within variants). Expressing changes of representation as explicit conversions warns the user of the potentially high cost of these operations.