Rationale for Ada 2012
3.4 Quantified expressions
Another new form of
expression in Ada 2012 is the quantified expression. The syntax is
quantified_expression ::=
for quantifier loop_parameter_specification => predicate
| for quantifier iterator_specification => predicate
quantifier ::= all | some
predicate ::= boolean_expression
The form involving
iterator_specification
concerns generalized iterators and will be found particularly useful
with containers; it will be discussed in detail in Section
6.3
on iteration. Here we will concentrate on the use of the familiar loop
parameter specification.
The type of a quantified
expression is Boolean. So we might write
B := (for all K in A'Range => A(K) = 0);
which assigns true
to B if every component of the array A
has value 0. We might also write
B := (for some K in A'Range => A(K) = 0);
which assigns true to B
if some component of the array A has value
0.
Note that the loop parameter is almost inevitably
used in the predicate. A quantified expression is very much like a for
statement except that we evaluate the expression after =>
on each iteration rather than executing one or more statements. The iteration
is somewhat implicit and the words loop and end loop do
not appear.
The expression is evaluated for each iteration in
the appropriate order (reverse can be inserted of course) and
the iteration stops as soon as the value of the expression is determined.
Thus in the case of for all, as soon as one value is found to
be False, the overall expression is False
whereas in the case of for some as soon as one value is found
to be True, the overall expression is True.
An iteration could raise an exception which would then be propagated
in the usual way.
Like conditional expressions, a quantified expression
is always enclosed in parentheses which can be omitted if the context
already provides them, such as in a procedure call with a single positional
parameter.
Incidentally, predicate is a fancy word meaning Boolean
expression. Older folk might recall that it also means the part of a
sentence after the subject. Thus in the sentence "I love Ada",
the subject is "I" and the predicate is "love Ada".
The forms
for all and
for some are
technically known as the universal quantifier and existential quantifier
respectively.
Note that some is a new reserved word (the
only one in Ada 2012). There were six new ones in Ada 95 (abstract,
aliased, protected, requeue, tagged and until)
and three new ones in Ada 2005 (interface, overriding and
synchronized). Hopefully we are converging.
The type of a quantified expression can be any Boolean
type (that is the predefined type Boolean
or perhaps My_Boolean derived from Boolean).
The predicate must be of the same type as the expression as a whole.
Thus if the predicate is of type My_Boolean
then the quantified expression is also of type My_Boolean.
The syntax for quantified expressions uses
=>
to introduce the predicate. This is similar to the established notation
in SPARK
[13]. Consideration was given
to using a vertical bar which is common in mathematics but that would
have been confusing because of its use in membership tests and other
situations with multiple choices.
As illustrated in the
Introduction (see
1.3.2), quantified expressions
will find their major uses in pre- and postconditions. Thus a procedure
Sort on an array
A
of type
Atype such as
type Atype is array (Index) of Float;
might have specification
procedure Sort(A: in out Atype)
with Post => A'Length < 2 or else
(for all K in A'First .. Index'Pred(A'Last) => A(K) <= A(Index'Succ(K)));
where we are assuming that the index type need not
be an integer type and so we have to use Succ
and Pred. Note how the trivial cases of a
null array or an array with a single component are dismissed first.
Quantified expressions
can be nested. So we might check that all components of a two-dimensional
array are zero by writing
B := (for all I in AA'Range(1) =>
(for all J in AA'Range(2) => AA(I, J) = 0));
This can be done rather
more neatly using the syntactic form
for quantifier
iterator_specification =>
predicate
as will be discussed
in detail in Section
6.3 on iteration. We
just write
B := (for all E of AA => E = 0);
which iterates over all elements of the array AA
however many dimensions it has.
© 2011, 2012, 2013 John Barnes Informatics.
Sponsored in part by: