Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
 
Annotated Ada Reference ManualLegal Information
Contents   Index   References   Search   Previous   Next 

3.2.4 Subtype Predicates

1/3
{AI05-0153-3} {AI05-0269-1} {AI05-0299-1} 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). 
1.a/3
Aspect Description for Static_Predicate: Condition that must hold true for objects of a given subtype; the subtype may be static.
1.b/3
Aspect Description for Dynamic_Predicate: Condition that must hold true for objects of a given subtype; the subtype is not static.

Name Resolution Rules

2/3
{AI05-0153-3} The expected type for a predicate aspect expression is any boolean type.

Static Semantics

3/3
{AI05-0153-3} 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: 
4/4
{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.
5/3
For a subtype created by a subtype_indication, the predicate of the subtype denoted by the subtype_mark applies. 
6/4
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)].
7/3
{AI05-0290-1} Predicate checks are defined to be enabled or disabled for a given subtype as follows:
8/3
If a subtype is declared by a type_declaration or subtype_declaration that includes a predicate specification, then: 
9/3
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;
10/3
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;
11/3
otherwise, predicate checks are disabled for the subtype[, regardless of whether predicate checking is enabled for any other subtypes mentioned in the declaration]; 
12/4
{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;
13/3
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;
14/3
Otherwise, predicate checks are disabled for the given subtype.
14.a/3
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.
14.b/4
{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. 
14.1/4
   {AI12-0054-2} 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):
14.2/4
   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. 
14.b.1/4
Aspect Description for Predicate_Failure: Action to be performed when a predicate check fails.

Name Resolution Rules

14.3/4
   {AI12-0054-2} The expected type for the Predicate_Failure expression is String. 

Legality Rules

15/3
 {AI05-0153-3} {AI05-0269-1} The expression of a Static_Predicate specification shall be predicate-static; that is, one of the following:
16/3
a static expression;
17/4
{AI12-0039-1} a membership test whose tested_simple_expression simple_expression is the current instance, and whose membership_choice_list meets the requirements for a static membership test (see 4.9);
18/3
a case_expression whose selecting_expression is the current instance, and whose dependent_expressions are static expressions;
19/3
a call to a predefined equality or ordering operator, where one operand is the current instance, and the other is a static expression;
20/4
{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;
21/3
{AI05-0269-1} a short-circuit control form where both operands are predicate-static; or
22/3
a parenthesized predicate-static expression.
23/3
 {AI05-0262-1} A predicate shall not be specified for an incomplete subtype.
23.a/3
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. 
24/3
 {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.
24.a/3
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: 
24.b/3
   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!
25/3
 {AI05-0153-3} An index subtype, discrete_range of an index_constraint or slice, or a discrete_subtype_definition of a constrained_array_definition, entry_declaration, or entry_index_specification shall not denote a subtype to which predicate specifications apply.
26/3
 {AI05-0153-3} The prefix of an attribute_reference whose attribute_designator is First, Last, or Range shall not denote a scalar subtype to which predicate specifications apply.
26.a/3
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. 
27/3
 {AI05-0153-3} {AI05-0262-1} {AI05-0287-1} The discrete_subtype_definition of a loop_parameter_specification shall not denote a nonstatic subtype to which predicate specifications apply or any subtype to which Dynamic_Predicate specifications apply.
28/3
 {AI05-0153-3} {AI05-0262-1} The discrete_choice of a named_array_aggregate shall not denote a nonstatic subtype to which predicate specifications apply.
28.a/3
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. 
29/3
 {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

29.1/4
   {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.
29.a/4
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. 
29.2/4
   {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:
29.3/4
the value is first tested to determine whether it satisfies any constraints or any null exclusion of S;
29.4/4
then:
29.5/4
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);
29.b/4
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. 
29.6/4
if S is defined by a subtype_indication, the value is tested to determine whether it satisfies the predicates of the subtype denoted by the subtype_mark of the subtype_indication;
29.7/4
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. 
29.b.1/4
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. 
30/3
 {AI05-0153-3} {AI05-0290-1} If predicate checks are enabled for a given subtype, then: 
31/4
{AI12-0054-2} {AI12-0071-1} [On 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. 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 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 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.
31.1/4
{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.
31.a/3
Ramification: Predicates are not evaluated at the point of the (sub)type declaration. 
31.b/3
Implementation Note: Static_Predicate checks can be removed even in the presence of potentially invalid values, just as constraint checks can be removed. 
31.c/4
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.
32/4
 This paragraph was deleted.{AI05-0262-1} {AI125-0071} A value satisfies a predicate if the predicate is True for that value.
33/4
 This paragraph was deleted.{AI05-0153-3} {AI05-0276-1} {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.
33.a/4
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. 
NOTES
34/3
5  {AI05-0153-3} A predicate specification does not cause a subtype to be considered constrained.
35/3
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.
36/4
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.
37/4
8  {AI12-0054-2} Predicate_Failure expressions are never evaluated during the evaluation of a membership test (see 4.5.2) or Valid attribute (see 13.9.2).
38/4
9  {AI12-0054-2} A Predicate_Failure expression can be a raise_expression (see 11.3). 

Examples

39/4
{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' | 'Æ' | 'æ' | 'Ð' | 'ð' | 'Þ' | 'þ' | 'ß';
40/4
{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";
41/4
 {AI12-0054-2} Text_IO (see A.10.1) could have used predicates to describe some common exceptional conditions as follows:
42/4
with Ada.IO_Exceptions;
package Ada.Text_IO is
43/4
   type File_Type is limited private;
44/4
   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);
45/4
   ...
46/4
   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;
47/4
   ...
48/4
   procedure Get (File : in Input_File_Type; Item : out Character);
49/4
   procedure Put (File : in Output_File_Type; Item : in Character);
50/4
   ...
51/4
   -- Similarly for all of the other input and output subprograms.

Extensions to Ada 2005

51.a/3
{AI05-0153-3} {AI05-0262-1} {AI05-0276-1} {AI05-0290-1} Predicate aspects are new in Ada 2012. 

Extensions to Ada 2012

51.b/4
{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

51.c/4
{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.
51.d/4
{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.
51.e/4
{AI12-0099-1} Corrigendum: Revised wording to list the boolean operators that can be predicate-static, to eliminate confusion about whether not is included. 

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe