Rationale for Ada 2012

John Barnes
Contents   Index   References   Search   Previous   Next 

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.

Contents   Index   References   Search   Previous   Next 
© 2011, 2012, 2013 John Barnes Informatics.
Sponsored in part by:
The Ada Resource Association:

    ARA
  AdaCore:


    AdaCore
and   Ada-Europe:

Ada-Europe