Ada Reference Manual (Ada 2022) — Legal Information

4.5.8 Quantified Expressions

Quantified expressions provide a way to write universally and existentially quantified predicates over containers and arrays.

Syntax

1/3

quantified_expression ::=
for quantifier loop_parameter_specification => predicate
| for quantifier iterator_specification => predicate

2/3

quantifier ::= all | some

3/3

predicate ::= boolean_expression

4/3

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.

Name Resolution Rules

5/3

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

6/5

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 (see 5.5 and 5.5.2).

7/3

The value of the quantified_expression is determined as follows:

8/4

If the quantifier is all, the expression is False if the evaluation of any 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. Any exception raised by evaluation of the predicate is propagated.

9/4

If the quantifier is some, the expression is True if the evaluation of any 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. Any exception raised by evaluation of the predicate is propagated.

Examples

10/5

Example of a quantified expression as a postcondition for a sorting routine on an array A with an index subtype T:

11/3

Post => (A'Length < 2 or else
(for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))

12/5

Example of use of a quantified expression as an assertion that a positive number N is composite (as opposed to prime):

13/5

pragma Assert (for some X in 2 .. N when X * X <= N => N mod X = 0);
-- see iterator_filter in 5.5

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