3.2.4 Subtype Predicates
for Static_Predicate: Condition
that must hold true for objects of a given subtype; the subtype may be
for Dynamic_Predicate: Condition
that must hold true for objects of a given subtype; the subtype is not
Name Resolution Rules
For a (first) subtype defined
by a derived type declaration, the predicates of the parent subtype and
the progenitor subtypes apply.
The predicate of a subtype consists of all
predicate specifications that apply, and-ed together; if no predicate
specifications apply, the predicate is True [(in particular, the predicate
of a base subtype is True)].
Predicate checks are defined to be enabled
or disabled for a given subtype as follows:
if performing checks
is required by the Static_Predicate assertion policy (see 11.4.2)
and the declaration includes a Static_Predicate specification, then predicate
checks are enabled for the subtype;
if performing checks
is required by the Dynamic_Predicate assertion policy (see 11.4.2)
and the declaration includes a Dynamic_Predicate specification, then
predicate checks are enabled for the subtype;
checks are disabled for the subtype[, regardless of whether predicate
checking is enabled for any other subtypes mentioned in the declaration];
If a subtype is defined by
a derived type declaration that does not include a predicate specification,
then predicate checks are enabled for the subtype if and only if predicate
checks are enabled for at least one of the parent subtype and the progenitor
If a subtype is created by
other than in one of the previous cases, then predicate checks are enabled
for the subtype if and only if predicate checks are enabled for the subtype
denoted by the subtype_mark;
Otherwise, predicate checks
are disabled for the given subtype.
this case, no predicate specifications can apply to the subtype and so
it doesn't typically matter whether predicate checks are enabled. This
rule does make a difference, however, when determining whether predicate
checks are enabled for another type when this type is one of multiple
progenitors. See the “derived type declaration” wording above.
Even when predicate checks
are disabled, a predicate cam affect various Legality Rules, the results
of membership tests, the items in a for loop, and the result of
the Valid attribute.
a static expression;
a call to a predefined equality
or ordering operator, where one operand is the current instance, and
the other is a static expression;
a call to a predefined boolean logical operator,
where each operand is predicate-static;
a short-circuit control form where both operands
are predicate-static; or
A predicate shall not be specified for an incomplete
Reason: The expression
of such a predicate could not depend on the properties of the value of
the type (since it doesn't have any), so it is useless and we don't want
to require the added complexity needed to support it.
If a predicate applies to a subtype, then that
predicate shall not mention any other subtype to which the same predicate
This is intended to prevent recursive predicates, which cause definitional
problems for static predicates. Inside of the predicate, the subtype
name refers to the current instance of the subtype, which is an object,
so a direct use of the subtype name cannot be recursive. But other subtypes
naming the same type might:
type Really_Ugly is private;
subtype Ugly is Really_Ugly;
type Really_Ugly is new Integer
with Static_Predicate => Really_Ugly not in Ugly; -- Illegal!
This is to prevent confusion about whether the
First value is the lowest value of the subtype (which does not depend
on the predicate) or the lowest value of the subtype which meets the
predicate. (For a dynamic predicate, determining this latter value is
expensive as it would usually require a loop.) For a static subtype that
has a static predicate, the First_Valid and Last_Valid attributes (see
3.5.5) can be used instead.
This rule prevents noncontiguous dynamically bounded
array aggregates, which could be expensive to check for. (Array aggregates
have rules to prevent problems with static subtypes.) We define this
rule here so that the runtime generic body check applies.
In addition to the places where Legality Rules
normally apply (see 12.3), these rules apply
also in the private part of an instance of a generic unit.
[On every subtype conversion,
the predicate of the target subtype is evaluated, and a check is performed
that the predicate is True. This includes all parameter passing, except
for certain parameters passed by reference, which are covered by the
following rule: ] After normal completion and leaving of a subprogram,
for each in out or out parameter that is passed by reference,
the predicate of the subtype of the actual is evaluated, and a check
is performed that the predicate is True. For an object created by an
with no explicit initialization expression,
or by an uninitialized allocator,
if any subcomponents have default_expressions,
the predicate of the nominal subtype of the created object is evaluated,
and a check is performed that the predicate is True. Assertions.Assertion_Error
is raised if any of these checks fail.
are not evaluated at the point of the (sub)type declaration.
Static_Predicate checks can be removed even in the presence of potentially
invalid values, just as constraint checks can be removed.
A value satisfies a predicate if the predicate
is True for that value.
If any of the above Legality Rules is violated
in an instance of a generic unit, Program_Error is raised at the point
of the violation.
is the usual way around the contract model; this applies even in instance
bodies. Note that errors in instance specifications will be detected
at compile-time by the "re-check" of the specification, only
errors in the body should raise Program_Error.
A predicate specification does not cause a subtype
to be considered constrained.
A Static_Predicate, like a constraint, always remains
True for all objects of the subtype, except in the case of uninitialized
variables and other invalid values. A Dynamic_Predicate, on the other
hand, is checked as specified above, but can become False at other times.
For example, the predicate of a record subtype is not checked when a
subcomponent is modified.
Extensions to Ada 2005
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe