Quantified Expressions

{AI12-0158-1} Quantified expressions provide a way to write universally and existentially quantified predicates over containers and arrays.

Syntax

{AI05-0176-1} Wherever the Syntax Rules allow an expression, a quantified_expression may be used in place of the expression, so long as it is immediately surrounded by parentheses.

Discussion: The syntactic category quantified_expression appears only as a primary that is parenthesized. The above rule allows it to additionally be used in other contexts where it would be directly surrounded by parentheses. This is the same rule that is used for conditional_expressions; see 4.5.7 for a detailed discussion of the meaning and effects of this rule.

Name Resolution Rules

{AI05-0176-1} The expected type of a quantified_expression is any Boolean type. The predicate in a quantified_expression is expected to be of the same type.

Dynamic Semantics

{AI05-0176-1} {AI12-0158-1} {AI12-0327-1} For the evaluation of a quantified_expression, the loop_parameter_specification or iterator_specification is first elaborated. The evaluation of a quantified_expression then performs an iteration, and evaluates the predicate for each value conditionally produced by the iteration the values each value of the loop parameter. These values are examined in the order specified by the loop_parameter_specification (see 5.5 and) or iterator_specification (see 5.5.2).

Ramification: {AI12-0327-1} The order of evaluation of the predicates is that in which the values are produced, as specified in 5.5 or 5.5.2.

{AI12-0158-1} If the quantifier is all, the expression is False True if the evaluation of any the predicate yields False; evaluation of the quantified_expression stops at that point. Otherwise (every predicate has been evaluated and yielded True), the expression is True True for each value of the loop parameter. It is False otherwise. Evaluation of the quantified_expression stops when all values of the domain have been examined, or when the predicate yields False for a given value. Any exception raised by evaluation of the predicate is propagated.

{AI12-0158-1} If the quantifier is some, the expression is True if the evaluation of any the predicate yields True; evaluation of the quantified_expression stops at that point. Otherwise (every predicate has been evaluated and yielded False), the expression is False for some value of the loop parameter. It is False otherwise. Evaluation of the quantified_expression stops when all values of the domain have been examined, or when the predicate yields True for a given value. Any exception raised by evaluation of the predicate is propagated.

Examples

{AI05-0176-1} {AI12-0429-1} Example of a quantified expression as a postcondition for a sorting routine on an array A with an index subtype T: The postcondition for a sorting routine on an array A with an index subtype T can be written:

{AI05-0176-1} {AI12-0429-1} {AI12-0430-1} Example of use of a quantified expression as an assertion that a positive number N is composite (as opposed to prime): The assertion that a positive number is composite (as opposed to prime) can be written:

{AI12-0312-1} pragma Assert (for some X in 2 .. N when X * X <= N / 2 => N mod X = 0);
-- see iterator_filter in 5.5

Extensions to Ada 2005

Wording Changes from Ada 2012

{AI12-0158-1} Corrigendum: Revised the wording to make it clear that the semantics is short-circuited, and what the result is when there are no values for the loop parameter.