Ada Reference Manual (Ada 2022)
4.5.8 Quantified Expressions
Quantified expressions provide a way to write universally and existentially quantified predicates over containers and arrays.
Syntax
quantified_expression ::=
for quantifier loop_parameter_specification => predicate
| for quantifier iterator_specification => predicate
for quantifier loop_parameter_specification => predicate
| for quantifier iterator_specification => predicate
quantifier ::= all | some
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
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
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).
The value of the quantified_expression is determined as follows:
- 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.
- 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
Example of a quantified expression as a postcondition for a sorting routine on an array A with an index subtype T:
Post => (A'Length < 2 or else
(for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))
(for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))
Example of use of a quantified expression as an assertion that a positive number N is composite (as opposed to prime):
