Ada Reference Manual (Ada 2022) — Legal Information

# 4.5.8 Quantified Expressions

0.1/4
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