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
-but the vertical bar has already other uses in Ada syntax.
+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