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

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

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

Static case expressions are valuable because they provide the comfort of covering all values of the current instance. Suppose we have a type Animal

We could then declare a subtype of friendly animals

and perhaps

or equivalently

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

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

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

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

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

and then

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

and the subtype predicate will be checked on the call of Do_Date. However, beware that if we write

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

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

Note that it would be neater to write

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

and so on. Or we could even use a quantified expression

or go all the way in one lump

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

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

then we cannot write

However, a subtype with a static predicate can be used in a for loop thus

and in a named aggregate such as

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

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

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

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

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

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

can be implemented simply as a sequence of 43 iterations. However, a loop such as

which might look innocuous requires iterating over the whole set of integers. Thus we insist on having to write

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

and then

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

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.

© 2011, 2012, 2013 John Barnes Informatics.

Sponsored in part by: