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