4.5.8 Quantified Expressions
{
AI12-0158-1}
Quantified expressions provide a way to write universally
and existentially quantified predicates over containers and arrays.
Syntax
quantifier ::= all |
some
Discussion: The syntactic category
quantified_expression
appears only as a
primary
that is parenthesized. The above rule allows it to additionally be used
in other contexts where it would be directly surrounded by parentheses.
This is the same rule that is used for
conditional_expressions;
see
4.5.7 for a detailed discussion of the
meaning and effects of this rule.
Name Resolution Rules
Dynamic Semantics
Ramification: {
AI12-0327-1}
The order of evaluation of the predicates is that
in which the values are produced, as specified in 5.5
or 5.5.2.
{
AI12-0158-1}
If the
quantifier
is
all, the expression is
False True
if the evaluation of
any the
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 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.
Ramification: The
expression
is True if the domain contains no values.
{
AI12-0158-1}
If the
quantifier
is
some, the expression is True if the evaluation of
any the
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 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.
Ramification: The
expression
is False if the domain contains no values.
Examples
{
AI05-0176-1}
{
AI12-0429-1}
Example of a quantified expression as a postcondition
for a sorting routine on an array A with an index subtype T: The
postcondition for a sorting routine on an array A with an index subtype
T can be written:
Post => (A'Length < 2 or else
(for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))
{
AI05-0176-1}
{
AI12-0429-1}
{
AI12-0430-1}
Example of use of a quantified expression as
an assertion that a positive number N is composite (as opposed to prime): The
assertion that a positive number is composite (as opposed to prime) can
be written:
Extensions to Ada 2005
Wording Changes from Ada 2012
{
AI12-0158-1}
Corrigendum: Revised the wording to make
it clear that the semantics is short-circuited, and what the result is
when there are no values for the loop parameter.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe