4.5.8 Quantified Expressions
Quantified expressions provide a way to write universally
and existentially quantified predicates over containers and arrays.
Syntax
quantifier ::= all |
some
Name Resolution Rules
Dynamic Semantics
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.
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
Example of a quantified
expression as a postcondition for a sorting routine on an array A with
an index subtype T:
Post => (A'Length < 2 or else
(for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))
Example of use of
a quantified expression as an assertion that a positive number N is composite
(as opposed to prime):
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