Ada Reference Manual — Legal Information
Contents   Index   References   Search   Previous   Next 

4.5.8 Quantified Expressions

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/3
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 each value of the loop parameter. These values are examined 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/3
If the quantifier is all, the expression is True if the evaluation of the predicate yields True for each value of the loop parameter. It is False otherwise. Evaluation of the quantified_expression stops when all values of the domain have been examined, or when the predicate yields False for a given value. Any exception raised by evaluation of the predicate is propagated.
9/3
If the quantifier is some, the expression is True if the evaluation of the predicate yields True for some value of the loop parameter. It is False otherwise. Evaluation of the quantified_expression stops when all values of the domain have been examined, or when the predicate yields True for a given value. 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