# CVS difference for ai05s/ai05-0176-1.txt

Differences between 1.17 and version 1.18
Log of other versions for file ai05s/ai05-0176-1.txt

```--- ai05s/ai05-0176-1.txt	2010/10/26 05:39:47	1.17
+++ ai05s/ai05-0176-1.txt	2010/11/19 05:36:23	1.18
@@ -1,5 +1,4 @@
-!standard 1.1.4(12)                                    10-10-15  AI05-0176-1/09
-!standard 2.9(2/2)
+!standard 2.9(2/2)                                     10-11-18  AI05-0176-1/10
!standard 4.4(7)
!standard 4.5.9(0)
!reference AI05-0139-2
@@ -37,14 +36,12 @@
indicate the domain of definition of the element (which is some finite set).
The common notation is:

-    for all  X in domain | P (X)
+    for all  X in domain =>  P (X)

-[Editor's note: Change syntax to "=>"?? See e-mail of Sept. 15, 2010.]
-
Similarly, to indicate that at least one element of the domain satisfies a given
property, we might write

-    for some X in domain | P (X)
+    for some X in domain =>  P (X)

The domain can be a discrete range, or an expression that designates a
container. The first is typically used when the collection is an array, and the
@@ -54,7 +51,7 @@
directly an element of the collection, and we can use the proposed syntax of
AI05-0139-2 to write:

-    for all X of Directory | Name (X)'Length < 20
+    for all X of Directory => Name (X)'Length < 20

Where Directory is some container, or an array.

@@ -64,28 +61,22 @@
!proposal

Introduce quantified expressions in the language, with their usual meaning:
-boolean expressions that verify whether all (resp. at least one) element in a
-collection (array or container) satisfies a given predicate. Introduce a
-new reserved keyword: "some" to support this feature.
+they are boolean expressions that verify whether all (resp. at least one)
+element in a collection (array or container) satisfies a given predicate.
+Introduce a new reserved keyword: "some" to support this feature.

Quantified expressions have the following syntax:

-     ( for quantifier loop_parameter_specification | Boolean_Expression )
+     ( for quantifier loop_parameter_specification => Boolean_Expression )
or
-     ( for quantifier iterator_specification | Boolean_Expression )
+     ( for quantifier iterator_specification => Boolean_Expression )

The iterator_specification is the one proposed in AI05-0139-2 for
-iterators. It includes default iterations over discrete ranges and over
+iterators. It includes default iterations over discrete ranges, arrays, and
containers, as well as user-defined iterations over such.

!wording

-Modify 1.1.4(12):
-
-* A vertical line separates alternative items unless it occurs immediately
-  after an opening curly bracket{, a loop_parameter_specification, or an
-  iterator_specification}, in which case it stands for itself:
-
Add "some" to the list of reserved words in 2.9(2/2).

Add to 4.4 (7) a new kind of primary:
@@ -98,15 +89,11 @@

Syntax

-   quantified_expression ::= for quantifier loop_parameter_specification | predicate
-       |                     for quantifier iterator_specification | predicate
+   quantified_expression ::= for quantifier loop_parameter_specification => predicate
+       |                     for quantifier iterator_specification => predicate
quantifier            ::= all | some
predicate             ::= boolean_expression

-AARM Ramification: The vertical line ('|') between the loop_parameter_specification and the
-predicate is an explicit vertical line; it does not separate alternative items as it does
-elsewhere in the syntax. See 1.1.4.
-
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.
@@ -125,9 +112,10 @@
Dynamic Semantics

For the evaluation of a quantified_expression, the loop_parameter_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 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.1).

The value of the quantified_expression is determined as follows:

@@ -150,29 +138,27 @@
AARM ramification: The expression is False if the domain contains no values.
*Some* is sometimes called "exists" in mathematical logic.

-[Editor's note: This wording needs some description of how it works for an
-iterator_specification -- but we can't do that until AI05-0139-2 gets closer
-to completion.]
-
-
Examples

The postcondition for a sorting routine on an array A with an index subtype T can
be written:

-Post => (for all I in A'First .. T'Pred(A'Last) | A (I) <= A (T'Succ (I)))
+Post => (A'Length < 2
+    or else (for all I in A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))

The assertion that a positive number is composite (as opposed to prime) can be
written:

-   pragma Assert (for some X in 2 .. N / 2 | N mod X = 0);
+   pragma Assert (for some X in 2 .. N / 2 => N mod X = 0);

!discussion

-Instead of a vertical bar, we could use a colon or a right arrow to separate the
-iterator from the condition. The proposed notation is more common in mathematics
+We have adopted the right arrow (=>) as a separator between the iterator
+specification and the predicate. Other choices were suggested, but the arrow
+is already used for this purpose in SPARK, and it seems preferable to be
+consistent with this programming precedent, rather than with mathematical
+convention, which uses a vertical bar.

The order of evaluation is fixed by the iterator used in the
loop_parameter_specification or iterator_specification, so there is a
@@ -184,16 +170,7 @@

(See Wording.)

-!corrigendum 1.1.4(12)

-@drepl
-@xbullet<A vertical line separates alternative items unless it occurs immediately
-after an opening curly bracket, in which case it stands for itself:>
-@dby
-@xbullet<A vertical line separates alternative items unless it occurs immediately
-after an opening curly bracket, a @fa<loop_parameter_specification>, or
-an @fa<iterator_specification>, in which case it stands for itself:>
-
!corrigendum 2.9(2/2)

@dinsl
@@ -216,8 +193,8 @@

@s8<@i<Syntax>>

-@xcode<@fa<quantified_expression ::= >@ft<@b<for>>@fa< quantifier loop_parameter_specification | predicate
-   | >@ft<@b<for>>@fa< quantifier iterator_specification | predicate
+@xcode<@fa<quantified_expression ::= >@ft<@b<for>>@fa< quantifier loop_parameter_specification => predicate
+   | >@ft<@b<for>>@fa< quantifier iterator_specification => predicate
quantifier            ::= >@ft<@b<all>>@fa< | >@ft<@b<some>>@fa<
predicate             ::= >@ft<@i<boolean_>>@fa<expression>>

@@ -232,10 +209,11 @@

@s8<@i<Dynamic Semantics>>

-For the evaluation of a @fa<quantified_expression>, the @fa<loop_parameter_specification>
-is first elaborated. The evaluation of a @fa<quantified_expression> then evaluates
+For the evaluation of a @fa<quantified_expression>, the @fa<loop_parameter_specification> or
+@fa<iterator_specification> is first elaborated. The evaluation of a @fa<quantified_expression> then evaluates
the @fa<predicate> for each value of the loop parameter. These values are examined
-in the order specified by the @fa<loop_parameter_specification> (see 5.5).
+in the order specified by the @fa<loop_parameter_specification> (see 5.5)
+or @fa<iterator_specification> (see 5.5.1).

The value of the @fa<quantified_expression> is determined as follows:

@@ -258,18 +236,28 @@
The postcondition for a sorting routine on an array A with an index subtype T
can be written:

-@xcode<Post =@> (@b<for all> I @b<in> A'First .. T'Pred(A'Last) | A (I) <= A (T'Succ (I)))>
+@xcode<Post =@> (@b A'Length < 2
+   @b<or else> (@b<for all> I @b<in> A'First .. T'Pred(A'Last) => A (I) <= A (T'Succ (I))))>

The assertion that a positive number is composite (as opposed to prime) can be
written:

-@xcode<@b<pragma> Assert (@b<for some> X @b<in> 2 .. N / 2 | N @b<mod> X = 0);>
+@xcode<@b<pragma> Assert (@b<for some> X @b<in> 2 .. N / 2 => N @b<mod> X = 0);>

!ACATS test

Add an ACATS C-Test to test the syntax and semantics.

+!ASIS section
+
+New queries on quantified expressions:
+
+  Iterator_Specification
+  Loop_Parameter_Specification
+  Predicate
+  Quantifier
+
!appendix

From: Robert Dewar
@@ -2681,11 +2669,11 @@
From: Randy Brukardt
Sent: Friday, June 25, 2010  4:01 PM

-> 4.5.7(4.a/3)... This is the same rule that is used for
-> conditional_expressions; see 4.5.7 for a detailed discussion of the
+> 4.5.7(4.a/3)... 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.
->
-> Since this *is* 4.5.7, it seems strange to refer to this chapter in
+>
+> Since this *is* 4.5.7, it seems strange to refer to this chapter in
> the sentence above.

Actually, this cause is supposed to be numbered 4.5.9, and the above sentence refers
@@ -2693,8 +2681,8 @@
draft. For that reason, I couldn't use the appropriate cross-reference, either, so I
just left the reference and hopefully I'll remember to fix it in the future.

-> I would propose that to (9/3) a remark is added that "Some"
-> is what in mathematical logic is called "exists" and is the opposite
+> I would propose that to (9/3) a remark is added that "Some"
+> is what in mathematical logic is called "exists" and is the opposite
> of "all".

Probably a good idea.
@@ -3368,13 +3356,13 @@

John wrote in his editorial review:

-> This AI is very confused over whether the form with
-> iterator_specification is included or not. It is in  the !proposal.
-> And in the !wording where the (loathsome) modification to the stuff
-> about vertical line is described and in the syntax. But it is not in
+> This AI is very confused over whether the form with
+> iterator_specification is included or not. It is in  the !proposal.
+> And in the !wording where the (loathsome) modification to the stuff
+> about vertical line is described and in the syntax. But it is not in
> the dynamic semantics.
-> But in the !corrigendum it is in the vertical line stuff but not in
-> the syntax or dynamic semantics. So wording and corrigendum are
+> But in the !corrigendum it is in the vertical line stuff but not in
+> the syntax or dynamic semantics. So wording and corrigendum are
> inconsistent.

Given that "iterator_specification" is defined by an AI that is very much
@@ -3384,14 +3372,14 @@

---

-> I must say for the umpteenth time that I hate this syntax using the
-> vertical bar. The advantage of using "=>" instead seem to me to be so
-> manifestly obvious that I still find it unbelievable that we are still
+> I must say for the umpteenth time that I hate this syntax using the
+> vertical bar. The advantage of using "=>" instead seem to me to be so
+> manifestly obvious that I still find it unbelievable that we are still
> using teh wretched bar.

Well, I voted against both "|" and "=>", bar because this isn't an alterative
or "or"; and "=>" because it looks too much like a case statement or aggregate
-for my taste.
+for my taste.

Indeed, using "=>" would be very confusing with the aggregate syntax of

```

Questions? Ask the ACAA Technical Agent