3.2.4 Subtype Predicates
Aspect Description for Static_Predicate:
Condition that must hold true for objects of a given subtype; the
subtype may be static.
Aspect Description for Dynamic_Predicate:
Condition that must hold true for objects of a given subtype; the
subtype is not static.
Name Resolution Rules
Static Semantics
{
AI12-0071-1}
{
AI12-0099-1}
For a (first) subtype defined by a type declaration, any predicates of
parent or progenitor subtypes apply.
{
AI05-0290-1}
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;
otherwise, predicate checks are disabled
for the subtype[, regardless of whether predicate checking is enabled
for any other subtypes mentioned in the declaration];
{
AI12-0099-1}
If a subtype is defined by a type declaration that does not include a
predicate specification, then predicate checks are enabled for the subtype
if and only if any predicate checks are enabled for parent or progenitor
subtypes;
If a subtype is created by a
subtype_indication
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.
Discussion: In 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.
{
AI12-0071-1}
Even when predicate checks are disabled, a predicate can affect various
Legality Rules, the results of membership tests, the items in a
for
loop, and the result of the Valid attribute.
Predicate_Failure
This aspect shall be specified by an
expression,
which determines the action to be performed when a predicate check fails
because a directly-specified predicate aspect of the subtype evaluates
to False, as explained below.
Aspect Description for Predicate_Failure:
Action to be performed when a predicate check fails.
Name Resolution Rules
Legality Rules
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;
{
AI05-0262-1}
{
AI12-0099-1}
a call to a predefined boolean operator
and,
or,
xor,
or
not, where each operand is predicate-static;
{
AI05-0269-1}
a short-circuit control form where both operands are predicate-static;
or
{
AI05-0262-1}
A predicate shall not be specified for an incomplete subtype.
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.
{
AI05-0287-1}
If a predicate applies to a subtype, then that predicate shall not mention
any other subtype to which the same predicate applies.
Reason: 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;
private
subtype Ugly is Really_Ugly;
type Really_Ugly is new Integer
with Static_Predicate => Really_Ugly not in Ugly; -- Illegal!
Reason: {
AI05-0297-1}
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.
Reason: {
AI05-0262-1}
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.
{
AI05-0262-1}
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.
Dynamic Semantics
{
AI125-0071}
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.
Discussion: This 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.
{
AI12-0071-1}
To determine whether a value
satisfies the predicates of a subtype
S, the following tests are performed in the following order, until
one of the tests fails, in which case the predicates are not satisfied
and no further tests are performed, or all of the tests succeed, in which
case the predicates are satisfied:
the value is first tested to determine whether
it satisfies any constraints or any null exclusion of S;
then:
if S is a first subtype, the value
is tested to determine whether it satisfies the predicates of the parent
and progenitor subtypes (if any) of S (in an arbitrary order);
Ramification: This rule has an effect
for derived types (which have a parent subtype and may have progenitors)
and for task and protected types (which may have progentitors). Other
kinds of type declarations can have neither, and no test is required
for other first subtypes.
finally, if S is defined by a declaration
to which one or more predicate specifications apply, the predicates are
evaluated (in an arbitrary order) to test that all of them yield True
for the given value.
Discussion: It is important to stop on
the first of the above steps that fails, as later steps might presume
that the earlier steps had succeeded.
{
AI12-0054-2}
{
AI12-0071-1}
[On every subtype conversion, a check is performed that the operand satisfies
the predicates of the target subtype. 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,
a check is performed that the value of the parameter satisfies the predicates
of the subtype of the actual. For an object created by an
object_declaration
with no explicit initialization
expression,
or by an uninitialized
allocator,
if any subcomponents have
default_expressions,
a check is performed that the value of the created object satisfies the
predicates of the nominal subtype.
{
AI12-0054-2}
If any of the predicate checks fail, Assertion_Error is raised, unless
the subtype whose directly-specified predicate aspect evaluated to False
also has a directly-specified Predicate_Failure aspect. In that case,
the specified Predicate_Failure
expression
is evaluated; if the evaluation of the Predicate_Failure
expression
propagates an exception occurrence, then this occurrence is propagated
for the failure of the predicate check; otherwise, Assertion_Error is
raised, with an associated message string defined by the value of the
Predicate_Failure
expression.
In the absence of such a Predicate_Failure aspect, an implementation-defined
message string is associated with the Assertion_Error exception.
Ramification: Predicates are not evaluated
at the point of the (sub)type declaration.
Implementation Note: Static_Predicate
checks can be removed even in the presence of potentially invalid values,
just as constraint checks can be removed.
Implementation defined: The message string
associated with the Assertion_Error exception raised by the failure of
a predicate check if there is no applicable Predicate_Failure aspect.
This paragraph
was deleted.
5 {
AI05-0153-3}
A predicate specification does not cause a subtype to be considered constrained.
6 {
AI05-0153-3}
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.
7 {
AI12-0071-1}
No predicates apply to the base subtype of a scalar type; every value
of a scalar type
T is considered to satisfy the predicates of
T'Base.
Examples
{
AI12-0054-2}
subtype Basic_Letter
is Character --
See A.3.2 for "basic letter".
with Static_Predicate => Basic_Letter
in 'A'..'Z' | 'a'..'z' | 'Æ' | 'æ' | 'Ð' | 'ð' | 'Þ' | 'þ' | 'ß';
{
AI12-0054-2}
subtype Even_Integer
is Integer
with Dynamic_Predicate => Even_Integer
mod 2 = 0,
Predicate_Failure => "Even_Integer must be a multiple of 2";
{
AI12-0054-2}
Text_IO (see A.10.1) could have used
predicates to describe some common exceptional conditions as follows:with Ada.IO_Exceptions;
package Ada.Text_IO is
type File_Type is limited private;
subtype Open_File_Type is File_Type
with Dynamic_Predicate => Is_Open (Open_File_Type),
Predicate_Failure => raise Status_Error with "File not open";
subtype Input_File_Type is Open_File_Type
with Dynamic_Predicate => Mode (Input_File_Type) = In_File,
Predicate_Failure => raise Mode_Error with "Cannot read file: " &
Name (Input_File_Type);
subtype Output_File_Type is Open_File_Type
with Dynamic_Predicate => Mode (Output_File_Type) /= In_File,
Predicate_Failure => raise Mode_Error with "Cannot write file: " &
Name (Output_File_Type);
...
function Mode (File : in Open_File_Type) return File_Mode;
function Name (File : in Open_File_Type) return String;
function Form (File : in Open_File_Type) return String;
...
procedure Get (File : in Input_File_Type; Item : out Character);
procedure Put (File : in Output_File_Type; Item : in Character);
...
-- Similarly for all of the other input and output subprograms.
Extensions to Ada 2005
Extensions to Ada 2012
{
AI12-0054-2}
Corrigendum: The Predicate_Failure aspect
is new. We can consider this a correction as it is always possible for
implementers to add implementation-defined aspects, so the same is true
for language-defined aspects.
Wording Changes from Ada 2012
{
AI12-0071-1}
Corrigendum: Specified the order of evaluation of most predicates,
by defining the new term "satisfies the predicates of the subtype".
This is not inconsistent, as the order previously was unspecified, so
any code depending on the order was incorrect. The change is necessary
so that the Predicate_Failure aspect has consistent results in cases
where multiple predicates and aspects apply; see the Ada.Text_IO example
above for such a case.
{
AI12-0099-1}
Corrigendum: Revised wording to ensure all kinds of types are
covered, including the anonymous task associated with a
single_task_declaration,
and generalized it.
{
AI12-0099-1}
Corrigendum: Revised wording to list the boolean operators that
can be predicate-static, to eliminate confusion about whether
not
is included.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
