Ada Reference Manual — 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/4
For the evaluation of a quantified_expression, the loop_parameter_specification or iterator_specification is first elaborated. The evaluation of a quantified_expression then evaluates the predicate for the values of the loop parameter in the order specified by the loop_parameter_specification (see 5.5) or iterator_specification (see 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/3
The postcondition for a sorting routine on an array A with an index subtype T can be written:
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/3
The assertion that a positive number is composite (as opposed to prime) can be written:
13/3
pragma Assert (for some X in 2 .. N / 2 => N mod X = 0);
Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe