Rationale for Ada 2012

John Barnes
Contents   Index   References   Search   Previous   Next 

2.5 Subtype predicates

The final major facility to be discussed here is subtype predicates. These are not really contractual in the sense that preconditions, postconditions and invariants are contractual but are more akin to constraints.
Subtype predicates are of two kinds, Static_Predicate and Dynamic_Predicate. They can be applied to subtype declarations and to type declarations using aspect specifications. For example, in the Introduction we met
subtype Even is Integer
   with Dynamic_Predicate => Even mod 2 = 0;
subtype Winter is Month
   with Static_Predicate => Winter in Dec | Jan | Feb;
The predicates take an expression of a Boolean type and again we note the use of the subtype name to denote the current instance. In the case of Dynamic_Predicate, the expression can be any Boolean expression.
However, in the case of Static_Predicate, the expression is restricted and can only be
a static membership test where the choice is selected by the current instance,
a case expression whose dependent expressions are static and selected by the current instance,
a call of the predefined operations =, /=, <, <=, >, >= where one operand is the current instance,
an ordinary static expression, 
and, in addition, a call of a Boolean logical operator and, or, xor, not whose operands are such static predicate expressions, and, a static predicate expression in parentheses.
So we see that the predicate in the subtype Even cannot be a static predicate because the operator mod is not permitted with the current instance. But mod could be used in an inner static expression.
However, the predicate in the subtype Winter can be a static predicate because it takes the from of a membership test where the choice is selected by the current instance and whose individual items are static. Note that membership tests are considerably enhanced in Ada 2012; further details will be given in Section 3.6. Another useful example of this kind is
subtype Letter is Character
   with Static_Predicate => Letter in 'A' .. 'Z' | 'a' .. 'z';
Static case expressions are valuable because they provide the comfort of covering all values of the current instance. Suppose we have a type Animal
type Animal is
 (Bear, Cat, Dog, Horse, Wolf);
We could then declare a subtype of friendly animals
subtype Pet is Animal
   with Static_Predicate => Pet in Cat | Dog | Horse;
and perhaps
subtype Predator is Animal
   with Static_Predicate => not (Predator in Pet);
or equivalently
subtype Predator is Animal
   with Static_Predicate => Predator not in Pet;
Now suppose we add Rabbit to the type Animal. Assuming that we consider that rabbits are pets and not food, we should change Pet to correspond but we might forget with awkward results. Maybe we have a procedure Hunt which aims to eliminate predators
procedure Hunt(P: in out Predator);
and we will find that our poor rabbit is hunted rather than petted!
What we should have done is use a case expression controlled by the current instance thus
subtype Pet is Animal
   with Static_Predicate =>
      (case Pet is
                when Cat | Dog | Horse => True,
                when Bear | Wolf => False);
and now if we add Rabbit to Animal and forget to update Pet to correspond then the program will fail to compile.
Note that a similar form of if expression where the current instance has to be of a Boolean type would not be useful and so is excluded.
Static subtypes with static predicates can also be used in case statements. Thus elsewhere in the program we might have
case Animal is
   when Pet =>    ...    -- feed it
   when Predator =>    ...    -- feed on it
end case;
Observe that we do not have to list all the individual animals and naturally there is no others clause. If other animals are added to Pet or Predator then this case statement will not need changing. Thus not only do we get the benefit of full coverage checking, but the code is also maintenance free. Of course if we add an animal that is neither a Pet nor Predator (Sloth perhaps?) then the case statement will need updating.
Subtype predicates, like pre- and postconditions and type invariants are similarly monitored by the pragma Assertion_Policy. If a predicate fails (that is, has value False) then Assertion_Error is raised.
Subtype predicates are checked in much the same sort of places as type invariants. Thus
on a subtype conversion,
on parameter passing (which covers expressions in general),
on default initialization of an object. 
Note an important difference from type invariants. If a type invariant is violated then the damage has been done. But subtype predicates are checked before any damage is done. This difference essentially arises because type invariants apply to private types and can become temporarily false inside the defining package as we saw with the procedure Flip applying to the type Disc_Pt.
If an object is declared without initialization and no default applies then any subtype predicate might be false in the same way that a subtype constraint might be violated.
Beware that subtype predicates like type invariants are not foolproof. Thus in the case of a record type they apply to the record as a whole but they are not checked if an individual component is modified.
Subtype predicates can be given for all types in principle. Thus we might have
type Date is
      D: Integer range 1 .. 31;
      M: Month;
      Y: Integer;
   end record;
and then
subtype Winter_Date is Date
   with Dynamic_Predicate => Winter_Date.M in Winter;
Note how this uses the subtype Winter which was itself defined by a subtype predicate. However, Winter_Date has to have a Dynamic_Predicate because the selector is not simply the current instance but a component of it.
We can now declare and manipulate a Winter_Date
WD: Winter_Date := (25, Dec, 2011);
and the subtype predicate will be checked on the call of Do_Date. However, beware that if we write
WD.Month := Jun;    -- dodgy
then the subtype predicate is not checked because we are modifying an individual component and not the record as a whole.
Subtype predicates can be given with type declarations as well as with subtype declarations. Consider for example declaring a type whose only allowed values are the possible scores for an individual throw when playing darts. These are 1 to 20 and doubles and trebles plus 50 and 25 for an inner and outer bull's eye. We could write these all out explicitly
type Score is new Integer
   with Static_Predicate => Score in 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12
                    | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21
                    | 22 | 24 | 25 | 26 | 27 | 28 | 30 | 32 | 33
                    | 34 | 36 | 38 | 39 | 40 | 42 | 45 | 48 | 50
                    | 51 | 54 | 57 | 60;
But that is rather boring and obscures the nature of the predicate. We can split it down by first defining individual subtypes for single, doubles and trebles as follows
subtype Single is Integer range 1 .. 20;
subtype Double is Integer
   with Static_Predicate =>
      Double in 2 | 4 | 6 | 8 | 10 | 12 | 14 | 16 | 18 | 20 | 22 | 24 | 26 | 28 | 30 | 32 | 34 | 36 | 38 | 40;
subtype Treble is Integer
   with Static_Predicate =>
      Treble in 3 | 6 | 9 | 12 | 15 | 18 | 21 | 24 | 27 | 30 | 33 | 36 | 39 | 42 | 45 | 48 | 51 | 54 | 57 | 60;
subtype Score is Integer
   with Static_Predicate =>
      Score in Single or Score in Double or
      Score in Treble or Score in 25 | 50;
Note that it would be neater to write
subtype Score is Integer
   with Static_Predicate =>
      Score in Single | Double | Treble | 25 | 50;
Observe that it does not matter that the individual predicates overlap. That is a score such as 12 is a Single, a Double and a Treble.
If we do not mind the predicates being dynamic then we can write
subtype Double is Integer
   with Dynamic_Predicate =>
      Double mod 2 = 0 and Double / 2 in Single;
and so on. Or we could even use a quantified expression
subtype Double is Integer
   with Dynamic_Predicate =>
      (for some K in Single => Double = 2*K);
or go all the way in one lump
type Dyn_Score is new Integer
   with Dynamic_Predicate =>
      (for some K in 1 .. 20 =>
         Score = K or Score = 2*K or Score = 3*K)
      or Score in 25 | 50;
There are some restrictions on the use of subtypes with predicates.
If a subtype has a static or dynamic predicate then it cannot be used as an array index subtype. This is to avoid arrays with holes. So we cannot write
type Winter_Hours is array (Winter) of Hours;    -- illegal
type Hits is array (Score range <>) of Integer;   -- illegal
Similarly, we cannot use a subtype with a predicate to declare the range of an array object or to select a slice. So if we have
type Month_Days is array (Month range <>) of Integer;
The_Days: Month_Days := (31, 28, 31, 30, ... );
then we cannot write
Winter_Days: Month_Days(Winter);    -- illegal array
The_Days(Winter) := (Jan | Dec => 31, Feb => 29);
                  -- really nasty illegal slice
However, a subtype with a static predicate can be used in a for loop thus
for W in Winter loop ...
and in a named aggregate such as
(Winter => 10.0, others => 14.0);  -- OK
but a subtype with a dynamic predicate cannot be used in these ways. Actually the restriction is slightly more complicated. If the original subtype is not static such as
subtype To_N is Integer range 1 .. N;
then even if To_N has a static predicate it still cannot be used in a for loop or named aggregate.
These rules can also be illustrated by considering the dartboard. We might like to accumulate a count of the number of times each particular score has been achieved. So we might like to declare
type Hit_Count is array (Score) of Integer;   -- illegal
but sadly this would result in an array with holes and so is forbidden. However, we could declare an array from 1 to 60 and then initialize it with 0 for those components used for hits and –1 for the unused components. Of course, we ought not to repeat literals such as 1 and 60 because of potential maintenance problems. But, we can use new attributes First_Valid and Last_Valid thus
type Hit_Count is array (Score'First_Valid .. Score'Last_Valid) of Integer :=
       (Score => 0, others => –1);
which uses Score to indicate the used components. The attributes First_Valid and Last_Valid can be applied to any static subtype but are particularly useful with static predicates.
In detail, First_Valid returns the smallest valid value of the subtype. It takes any range and/or predicate into account whereas First only takes the range into account. Similarly Last_Valid returns the largest value. Incidentally, they are illegal on null subtypes (because null subtypes have no valid values at all).
The Hit_Count array can then be updated by the value of each hit as expected
A_Hit: Score := ... ;      -- next dart
Hit_Count(A_Hit) := Hit_Count(A_Hit) + 1;
If we attempt to assign a value of type Integer which is not in the subtype Score to A_Hit then Assertion_Error is raised.
After the game, we can now loop through the subtype Score and print out the number of times each hit has been achieved and perhaps accumulate the total at the same time thus
for K in Score loop
   New_Line;  Put(Hit);  Put(Hit_Count(K));
   Total := Total + K * Hit_Count(K);
end loop;
The reason for the distinction between static and dynamic predicates is that the static form can be implemented as small sets with static operations on the small sets. Hence the loop
for K in Score loop ...
can be implemented simply as a sequence of 43 iterations. However, a loop such as
for X in Even loop ...
which might look innocuous requires iterating over the whole set of integers. Thus we insist on having to write
for X in Integer loop
   if X in Even then ...
which makes the situation quite clear.
Another restriction on the use of subtypes with predicates is that the attributes First, Last and Range cannot be applied. But Pred and Succ are permitted because they apply to the underlying type. As a consequence, if a generic body uses First, Last or Range on a formal type and the actual type has a subtype predicate then Program_Error is raised.
Subtype predicates can be applied to abstract types but not to incomplete types.
Subtype predicates are inherited as expected on derivation. Thus if we have
type T is
   with Static_Predicate => SP(T);
and then
type NT is new T
   with Dynamic_Predicate => DP(NT);
the result is that both predicates apply to NT rather as if we had written the predicate as SP(NT) and DP(NT). So if several apply they are anded together. If any one is dynamic then restrictions on the use of subtypes with a dynamic predicate apply.
There is no need for special predicates for class wide types in the way that we have both Type_Invariant and Type_Invariant'Class. So in the general case where a tagged type is derived from a parent and several progenitors
type T is new P and G1 and G2 with ...
where P is the parent and G1 and G2 are progenitors, the subtype predicate applicable to T is simply those for P, G1 and G2 all anded together.
A number of improvements were made in this area after ISO standardization as described in Section 9.5 of the Epilogue. These concern a new aspect Predicate_Failure which enables specific messages to be associated with a failure and rules regarding the order of evaluation of predicates if several apply.

Contents   Index   References   Search   Previous   Next 
© 2011, 2012, 2013 John Barnes Informatics.
Sponsored in part by:
The Ada Resource Association:


and   Ada-Europe: