Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
 
Ada Reference Manual (Ada 2022)Legal Information
Contents   Index   References   Search   Previous   Next 

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

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe