3.2.4 Subtype Predicates
The language-defined
predicate aspects Static_Predicate
and Dynamic_Predicate may be used to define properties of subtypes. A
predicate specification is an
aspect_specification
for one of the two predicate aspects.
General rules for aspects and
aspect_specifications
are found in Clause
13 (
13.1
and
13.1.1 respectively).
Name Resolution Rules
The expected type for a predicate aspect
expression
is any boolean type.
Static Semantics
A predicate specification
may be given on a
type_declaration
or a
subtype_declaration,
and applies to the declared subtype. In addition, predicate specifications
apply to certain other subtypes:
For a (first) subtype defined by a type declaration,
any predicates of parent or progenitor subtypes apply.
This paragraph was
deleted.
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;
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.
For a subtype with a directly-specified predicate
aspect, the following additional language-defined aspect may be specified
with an
aspect_specification
(see
13.1.1):
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.
Name Resolution Rules
The expected type for the Predicate_Failure
expression
is String.
Legality Rules
The
expression
of a Static_Predicate specification shall be
predicate-static;
that is, one of the following:
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 operator and,
or, xor, or not, 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
subtype.
If a predicate applies to a subtype, then that predicate
shall not mention any other subtype to which the same predicate 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.
Dynamic Semantics
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.
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);
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.
If predicate checks
are enabled for a given subtype, then:
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.
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.
This paragraph was
deleted.
This paragraph was
deleted.
5 A predicate specification does not cause
a subtype to be considered constrained.
6 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 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.
8 Predicate_Failure
expressions
are never evaluated during the evaluation of a membership test (see
4.5.2)
or Valid attribute (see
13.9.2).
Examples
subtype Basic_Letter
is Character --
See A.3.2 for "basic letter".
with Static_Predicate => Basic_Letter
in 'A'..'Z' | 'a'..'z' | 'Æ' | 'æ' | 'Ð' | 'ð' | 'Þ' | 'þ' | 'ß';
subtype Even_Integer is Integer
with Dynamic_Predicate => Even_Integer mod 2 = 0,
Predicate_Failure => "Even_Integer must be a multiple of 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.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe