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

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

--- ai05s/ai05-0176-1.txt	2010/07/27 02:09:32	1.15
+++ ai05s/ai05-0176-1.txt	2010/10/16 06:14:07	1.16
@@ -1,9 +1,11 @@
-!standard 1.1.4(12)                                    10-07-26  AI05-0176-1/08
+!standard 1.1.4(12)                                    10-10-15  AI05-0176-1/09
 !standard 2.9(2/2)
 !standard 4.4(7)
 !standard 4.5.9(0)
+!reference AI05-0139-2
 !class Amendment 09-10-28
 !status Amendment 2012 10-06-03
+!status work item 10-10-15
 !status ARG Approved  7-0-3  10-06-18
 !status work item 10-06-18 [rejected by WG 9]
 !status ARG Approved  6-1-3  10-02-27
@@ -35,8 +37,10 @@
 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
 
@@ -62,7 +66,7 @@
 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
-non-reserved keyword: "some" to support this feature.
+new reserved keyword: "some" to support this feature.
 
 Quantified expressions have the following syntax:
 
@@ -78,7 +82,7 @@
 
 Modify 1.1.4(12):
 
-* A vertical line separates alternative items unless it immediately occurs
+* 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:
 
@@ -145,6 +149,11 @@
 
 AARM ramification: The expression is False if the domain contains no values.
 
+[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
@@ -177,10 +186,10 @@
 !corrigendum 1.1.4(12)
 
 @drepl
-@xbullet<A vertical line separates alternative items unless it immediately occurs
+@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 immediately occurs
+@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:>
 
@@ -207,6 +216,7 @@
 @s8<@i<Syntax>>
 
 @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>>
 
@@ -3164,7 +3174,7 @@
 
 ****************************************************************
 
-From: Randy Brukardy
+From: Randy Brukardt
 Sent: Monday, July 26, 2010  9:12 PM
 
 > All of the iterator forms should be included in the
@@ -3176,3 +3186,185 @@
 
 ****************************************************************
 
+From: John Barnes
+Sent: Wednesday, September 15, 2010  10:10 AM
+
+I am usually reasonably placid over the changes proposed to Ada but I keep
+finding my blood pressure raised by quantified expressions. This has struck me
+twice in the past few days, once when reviewing AI-176 and now again when
+reviewing the parts of the RM that I have been allocated.
+
+I very strongly object to using the vertical bar to introduce the predicate as
+in (using the examples in the RM)
+
+for all I in A'First .. T'Pred(A'Last) | A(I) <= A(T'Succ(I))
+
+pragma Assert(for some X in 2 .. N/2 | N mod X = 0);
+
+There are several things I don't like
+
+*    it complicates the vertical bar rules in 1.1.4. It's bad enough that we
+     have a problem here anyway dating back to Ada 83 with the "following a
+     curly brace rule" but to make matters so much worse seems criminal to me.
+     In any event at least the curly brace rule is more of a punctuation thing
+     but here we are introducing a special rule just when the wretched bar
+     follows certain named productions. That seems so out of place in 1.1.4
+     right at the beginning of the RM when we have absolutely no idea what the
+     productions are for.
+
+*    the vertical bar smells of OR to me and there is no ORishness in this code
+
+*    it is said that some mathematics uses the vertical bar; however, we are not
+     writing mathematics but doing programming.
+
+*    the vertical bar is just too weak a symbol. We need something bigger and
+     bolder to separate the two parts of the quantified expression
+
+*    Spark has used the combination => for this purpose for many years and there
+     seems no reason why we should not be consistent with existing usage
+
+Note that the !discussion in the AI says
+
+Instead of a vertical bar, we could use a colon or a right arrow to separate the
+iterator from the condition. The proposed syntax is more common in mathematics
+but the vertical bar has already other uses in the Ada syntax.
+
+This seems to me to be arguing for not using the vertical bar and one expects
+this to be followed by another sentence coming to that conclusion. But it just
+stops.
+
+Another point is that we need to take care to make it clear what things are
+grouped together. The syntax in Spark puts the predicate in parentheses and that
+seems to me to be a good thing to do. So the above examples would look like
+
+for all I in A'First..T'Pred(A'Last) => (A(I) <= A(T'Succ(I)))
+
+pragma Assert(for some X in 2 .. N/2 => (N mod X = 0))
+
+This AI was sent back by WG9 last time in order to make "some" a proper reserved
+word. Perhaps we could give it another rethink.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, September 15, 2010  10:33 AM
+
+I have no problem with the "|" but I understand that others do.
+
+Taking our cue from existing SPARK syntax seems reasonable and using "=>" would
+be fine.
+
+I don't see the need for parenthesizing the predicate, since it can certainly be
+done when it helps readability, but given that the whole construct is
+parenthesized, it will be redundant in many cases.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, September 15, 2010  10:50 AM
+
+> This AI was sent back by WG9 last time in order to make "some" a
+> proper reserved word. Perhaps we could give it another rethink.
+
+I can live with "=>" instead of "|".
+
+I think requiring parens around the predicate would be annoying if the predicate
+is a primary:
+
+Assert(for all I in A'Range =>  Is_Good(A(I)));
+Assert(for all I in A'Range => (Is_Good(A(I))));
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Wednesday, September 15, 2010  12:34 PM
+
+The vertical bar is indeed standard mathematical usage, but I have no
+problem with other choices if there is such strong objection (and
+blood pressure issues). The most compelling argument is consistency
+with SPARK at this point, so I'll be happy to go with => .  I looked
+at what Z does, but they live in  their own beyond-ASCII world,
+including proper quantifier symbols.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Wednesday, September 15, 2010  12:44 PM
+
+> The vertical bar is indeed standard mathematical usage, but I have no
+> problem with other choices if there is such strong objection (and
+> blood pressure issues).
+
+Of course, there are three of us who could argue for compatibility with SETL
+;-), but I have no more serious objection to =>
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, September 15, 2010  12:55 PM
+
+I prefer the vertical bar (mathematics and setl familiarty I think), but I agree
+that SPARK compatibility is a strong argment and can live with =>
+
+****************************************************************
+
+From: John Barnes
+Sent: Wednesday, September 15, 2010  2:56 PM
+
+My blood pressure is now quite reduced with the thought that => would be
+acceptable. Although I would prefer the parens, I am happy to forego them. Spark
+does use a lot of parens - possibly Pascal influence. (That is the language
+Pascal and not M Leroy.)
+
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, September 15, 2010  3:22 PM
+
+I definitely do NOT like the junk extra parens
+
+****************************************************************
+
+From: Randy Brukardt
+Sent (privately): Saturday, September 15, 2010  12:53 AM
+
+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 
+> 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 
+> inconsistent.
+
+Given that "iterator_specification" is defined by an AI that is very much
+still under construction, I have no idea what could or should be written in
+the Dynamic Semantics. I surely don't want to repeat complex rules here.
+Therefore, I suggest that we table this AI until AI05-0139-2 is done.
+
+---
+
+> 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. 
+
+Indeed, using "=>" would be very confusing with the aggregate syntax of
+
+    (for I in Positive => Func(I))
+or
+    (for I in Arr_Type'Range => new D(I))
+
+which has been repeatedly proposed to allow initializations based on the
+array index (including today on comp.lang.ada, which is why I thought of it).
+
+But the SPARK argument does seems to be compelling.
+
+****************************************************************

Questions? Ask the ACAA Technical Agent