3.2.4 Subtype Predicates
Aspect Description
for Static_Predicate: Condition
that will must
hold true for objects of a given subtype; the subtype may be static.
Aspect Description
for Dynamic_Predicate: Condition
that will 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
derived type
declaration,
any the
predicates of
the parent
or subtype
and the progenitor subtypes apply.
This paragraph was
deleted.{
AI05-0153-3}
{
AI12-0071-1}
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)].
{
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
derived 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
at least
one of the parent
or subtype
and the 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 cam
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
logical 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
{
AI12-0071-1}
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 "recheck" 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:
{
AI12-0419-1}
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),
after a (view) conversion of the value to the corresponding parent or
progenitor type;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}
{
AI12-0301-1}
{
AI12-0333-1}
{
AI12-0432-1}
[On
a every
subtype conversion,
the predicate of the target
subtype is evaluated, and a check is performed that the
operand
satisfies the predicates of the target subtype predicate
is True, except for certain view conversions
(see 4.6).
This
includes all parameter passing, except for certain parameters passed
by reference, which are covered by the following rule:]
In
addition, after 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
value of the parameter satisfies the predicates
of the subtype of the actual predicate is
True. For an object created by an
object_declaration
with no explicit initialization
expression,
or by an uninitialized
allocator,
if
the types of any parts have specified Default_Value
or Default_Component_Value aspects, or any subcomponents have
default_expressions,
the predicate of the nominal subtype of the created
object is evaluated, and a check is performed that the
value
of the created object satisfies the predicates of the nominal subtype predicate
is True.
Assertions.Assertion_Error is raised
if any of these checks fail.Ramification: {
AI12-0333-1}
Most parameter passing is covered by the subtype
conversion rule: all inbound in and in out parameters are
converted to the formal subtype, and the copy-back for by-copy out
and in out parameters includes a conversion to the actual subtype.
The remaining parameter-passing cases are covered by special rules: by-reference
out and in out parameters by the rule given above, and
we don't want any predicate checks on inbound out parameters,
accomplished in part by a special rule in 4.6.
{
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.
Paragraphs
32 and 33 were moved above
{
AI05-0153-3}
{
AI05-0276-1}
{
AI12-0071-1}
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.This paragraph
was deleted.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.
NOTE 1 {
AI05-0153-3}
A predicate specification does not cause a subtype to be considered constrained.
NOTE 2 {
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.
NOTE 3 {
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-0429-1}
Examples of predicates applied to scalar types:{
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.
Discussion: We
didn't change the language-defined Text_IO this way for Ada 2022 as it
would be incompatible in marginal cases: these subprogram specifications
would not be subtype conformant with existing access-to-subprogram types,
so Put_Line'Access (for instance) would become illegal in existing code.
The gain would not be worth the disruption.
Extensions to Ada 2005
Inconsistencies With Ada 2012
{
AI12-0301-1}
Correction: Predicate
checks are now performed on default-initialized objects with parts that
have Default_Value or Default_Component_Value specified. This is consistent
with the handling of constraint checks for such objects; it is thought
that the omission was unintended. However, a program that declares such
an object and depends on there not being a predicate check in original
Ada 2012 will fail in Ada 2022. As these attributes were new in Ada 2012,
their use is uncommon, so we believe that this inconsistency will be
rare and more likely to catch a bug than create one. 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.{
AI12-0333-1}
{
AI12-0432-1}
Correction: Predicate checks are no longer
made for any inbound out parameters nor for the target of an assignment_statement
when it is a view conversion. The rule change for this is found in 4.6,
so the inconsistency is documented there.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
