Ada Reference Manual (Ada 2022) — Legal Information

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). The predicate aspects are assertion aspects (see 11.4.2). The predicate aspects are not inherited, but their effects are additive, as defined below.

Name Resolution Rules

2/3

The expected type for a predicate aspect expression is any boolean type.

Static Semantics

3/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

For a (first) subtype defined by a type declaration, any predicates of parent or 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.

7/3

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

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;

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.1/4

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.

Name Resolution Rules

14.3/4

The expected type for the Predicate_Failure expression is String.

Legality Rules

15/3

The expression of a Static_Predicate specification shall be predicate-static; that is, one of the following:

16/3

a static expression;

17/4

a membership test whose tested_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

a call to a predefined boolean operator and, or, xor, or not, where each operand is predicate-static;

21/3

a short-circuit control form where both operands are predicate-static; or

22/3

a parenthesized predicate-static expression.

23/3

A predicate shall not be specified for an incomplete subtype.

24/3

If a predicate applies to a subtype, then that predicate shall not mention any other subtype to which the same predicate applies.

25/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

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.

27/3

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

The discrete_choice of a named_array_aggregate shall not denote a nonstatic subtype to which predicate specifications apply.

29/3

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

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.2/4

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/5

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;

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.

30/3

If predicate checks are enabled for a given subtype, then:

31/5

On a subtype conversion, a check is performed that the operand satisfies the predicates of the target subtype, except for certain view conversions (see 4.6). In addition, 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 the types of any parts have specified Default_Value or Default_Component_Value aspects, or any subcomponents have default_expressions, a check is performed that the value of the created object satisfies the predicates of the nominal subtype.

31.1/4

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.

Paragraphs 32 and 33 were moved above

34/3

NOTE 1 A predicate specification does not cause a subtype to be considered constrained.

35/3

NOTE 2 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

NOTE 3 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

NOTE 4 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

NOTE 5 A Predicate_Failure expression can be a raise_expression (see 11.3).

Examples

39/5

Examples of predicates applied to scalar types:

40/4

subtype Basic_Letter is Character -- See A.3.2 for "basic letter".
with Static_Predicate => Basic_Letter in 'A'..'Z' | 'a'..'z' | 'Æ' |
'æ' | 'Ð' | 'ð' | 'Þ' | 'þ' | 'ß';

41/4

subtype Even_Integer is Integer
with Dynamic_Predicate => Even_Integer mod 2 = 0,
Predicate_Failure => "Even_Integer must be a multiple of 2";

42/4

Text_IO (see A.10.1) could have used predicates to describe some common exceptional conditions as follows:

43/4

with Ada.IO_Exceptions;
package Ada.Text_IO is

44/4

type File_Type is limited private;

45/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);

46/4

...

47/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;

48/4

...

49/4

procedure Get (File : in Input_File_Type; Item : out Character);

50/4

procedure Put (File : in Output_File_Type; Item : in Character);

51/4

...

52/4

-- Similarly for all of the other input and output subprograms.

Ada 2005 and 2012 Editions sponsored in part by Ada-Europe