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

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

--- ai05s/ai05-0176-1.txt	2010/07/08 01:19:03	1.14
+++ ai05s/ai05-0176-1.txt	2010/07/27 02:09:32	1.15
@@ -1,8 +1,10 @@
-!standard 1.1.4(12)                                    10-06-03  AI05-0176-1/07
+!standard 1.1.4(12)                                    10-07-26  AI05-0176-1/08
+!standard 2.9(2/2)
 !standard 4.4(7)
 !standard 4.5.9(0)
 !class Amendment 09-10-28
 !status Amendment 2012 10-06-03
+!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
 !status work item 09-10-28
@@ -65,8 +67,10 @@
 Quantified expressions have the following syntax:
 
      ( for quantifier loop_parameter_specification | Boolean_Expression )
+or
+     ( for quantifier iterator_specification | Boolean_Expression )
 
-The loop_parameter_specification is the one proposed in AI05-0139-2 for
+The iterator_specification is the one proposed in AI05-0139-2 for
 iterators. It includes default iterations over discrete ranges and over
 containers, as well as user-defined iterations over such.
 
@@ -75,8 +79,10 @@
 Modify 1.1.4(12):
 
 * A vertical line separates alternative items unless it immediately occurs
-  after an opening curly bracket{ or a loop_parameter_specification}, in
-  which case it stands for itself:
+  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:
    quantified_expression
@@ -89,11 +95,10 @@
 Syntax
 
    quantified_expression ::= for quantifier loop_parameter_specification | predicate
-   quantifier            ::= all | Some
+       |                     for quantifier iterator_specification | predicate
+   quantifier            ::= all | some
    predicate             ::= boolean_expression
 
-[Editor's Note: "Some" is not a reserved word and is not given in boldface.]
-
 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.
@@ -140,8 +145,6 @@
 
 AARM ramification: The expression is False if the domain contains no values.
 
-Note: Some is not a reserved word.
-
 Examples
 
 The postcondition for a sorting routine on an array A with an index subtype T can
@@ -162,9 +165,10 @@
 but the vertical bar has already other uses in Ada syntax.
 
 The order of evaluation is fixed by the iterator used in the
-loop_parameter_specification,  so there is a strong assumption of sequentiality.
-Not clear how to indicate that a quantified expression can be evaluated in
-parallel, given that we have no mechanism to parallelize loops either.
+loop_parameter_specification or iterator_specification, so there is a
+strong assumption of sequentiality. Not clear how to indicate that a quantified
+expression can be evaluated in parallel, given that we have no mechanism to
+parallelize loops either.
 
 !example
 
@@ -177,8 +181,13 @@
 after an opening curly bracket, in which case it stands for itself:>
 @dby
 @xbullet<A vertical line separates alternative items unless it immediately occurs
-after an opening curly bracket or a @fa<loop_parameter_specification>, in
-which case it stands for itself:>
+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
+@b<some>
 
 !corrigendum 4.4(7)
 
@@ -187,7 +196,7 @@
    @fa<numeric_literal | >@ft<@b<null>>@fa< | string_literal | aggregate>
  @fa<| name | qualified_expression | allocator | (expression)>>
 @dby
-@xcode<@fa<primary ::=> 
+@xcode<@fa<primary ::=>
    @fa<numeric_literal | >@ft<@b<null>>@fa< | string_literal | aggregate>
  @fa<| name | qualified_expression | allocator | (expression) | (quantified_expression)>>
 
@@ -198,7 +207,7 @@
 @s8<@i<Syntax>>
 
 @xcode<@fa<quantified_expression ::= >@ft<@b<for>>@fa< quantifier loop_parameter_specification | predicate
-quantifier            ::= >@ft<@b<all>>@fa< | >@ft<Some>@fa<
+quantifier            ::= >@ft<@b<all>>@fa< | >@ft<@b<some>>@fa<
 predicate             ::= >@ft<@i<boolean_>>@fa<expression>>
 
 Wherever the Syntax Rules allow an @fa<expression>, a @fa<quantified_expression> may be
@@ -226,27 +235,24 @@
   given value. Any exception raised by evaluation of the @fa<predicate> is
   propagated.>
 
-@xbullet<If the @fa<quantifier> is @fc<Some>, the expression is True if the evaluation of the
+@xbullet<If the @fa<quantifier> is @b<some>, the expression is True if the evaluation of the
   @fa<predicate> yields True for some value of the loop parameter. It is False
   otherwise. Evaluation of the @fa<quantified_expression> stops when all values
   of the domain have been examined, or when the @fa<predicate> yields True for a
   given value. Any exception raised by evaluation of the @fa<predicate> is
   propagated.>
 
-Notes:@hr
-Some is not a reserved word.
-
 @s8<@i<Examples>>
 
-The postcondition for a sorting routine on an array A with an index subtype T can
-be written:
+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)))>
 
 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
@@ -681,18 +687,18 @@
 From: Bob Duff
 Sent: Monday, March 16, 2009  5:15 PM
 
-> I'm sure you do, you just forgot! ...
+> I'm sure eou do, you just forgot! ...
 
 Thanks for the mathematical logic lesson, but I think you misunderstood what I
 meant.  ;-)
 
 I understand what universal quantifiers are in maths, and I haven't forgotten my
-logic course (at least, I haven't forgotten the basics).  I even taught this
+logic course (at least, I haven't forgotten therbasics).  I even taught this
 stuff to Bill some time ago, and he understands, for example, why "all pink
 unicorns are green" is true.
 
 What I meant is that I don't know how this stuff should be translated into a
-programming language, especially an imperative programming language like, say,
+programming language, especially an imeerative programming language like, say,
 Ada.  Given your recent comments, you are thinking that "for all" is just
 syntactic sugar for a loop.  No big deal But it sounded like Cyrille was
 thinking of something more "math-y".
@@ -1351,7 +1357,7 @@
 
 ****************************************************************
 
-From: Robert Dewar
+From: Robed; D**R
 Sent: Tuesday, November 17, 2009  12:09 PM
 
 > By the way, some people are fanatically opposed to semi-reserved
@@ -2630,7 +2636,8 @@
 From: Yannick Moy
 Sent: Friday, May 21, 2010  2:47 AM
 
-Looking at AI05-0176-1/06 2010-04-12 on Quantified expressions, I found a few typos:
+Looking at AI05-0176-1/06 2010-04-12 on Quantified expressions, I found a few
+typos:
 
 In !problem, I found 2 typos:
 
@@ -2644,6 +2651,528 @@
 
 that verify whether all (resp. al least one)
                                ^^ (at)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, July 8, 2010  2:31 PM
+
+Minor comments on the Quantified expressions AI:
+
+> Quantified expressions have the following syntax:
+>
+>      ( for quantifier loop_parameter_specification |
+> Boolean_Expression )
+
+> Syntax
+>
+>    quantified_expression ::= for quantifier loop_parameter_specification | predicate
+>    quantifier            ::= all | Some
+>    predicate             ::= boolean_expression
+>
+> [Editor's Note: "Some" is not a reserved word and is not given in
+> boldface.]
+
+"Some" is a keyword, and should appear in lowercase boldface when used as such.
+It would be a reserved word, except for compatibility. Programmers will do just
+fine if they think of it as a reserved word. It really looks silly to format
+"for all" and "for some" in two different styles!
+
+There should be another NOTE before 2.9(3), something like:
+
+    The keyword "some" is used in the syntax of quantified_expressions
+    (see 4.5.9), but it is not reserved.
+
+If there are others (I don't remember any), it could be:
+
+    The following keywords are used in the syntax, but are not reserved:
+    "some", "mumble", "bumble", "dumble".
+
+The existing NOTE 2.9(3) should be modified:
+
+3     8  Keywords appear in lower case boldface in this
+      International Standard, except when used in the designator of an
+      attribute (see 4.1.4). Lower case boldface is also used for a reserved
+      word in a string_literal used as an operator_symbol. This is merely a
+      convention - programs may be written in whatever typeface is desired and
+      available.
+
+No need to formally define "keyword" -- these are just NOTEs, and it's clear
+enough what it means from the new NOTE I suggested.
+
+I don't understand when parens are required around quantified_expressions, nor
+how the syntax rules specify that.  The first sentence quoted above shows
+parens, but I don't see them in the syntax rules.
+
+In the formatted version, the three syntax rules appear all on one line, and are
+therefore undecipherable.  The above quote is from the unformatted version.
+
+This AI is already ARG approved.  If my comments above are not controversial
+then I think they can be considered as editorial changes.
+
+If they ARE controversial, then I'll start pounding my shoe on the table.  ;-)
+
+****************************************************************
+
+From: John Barnes
+Sent: Thursday, July 8, 2010  2:42 PM
+
+The WG9 meeting in Valencia sent back AI-176 and directed the ARG to make some a
+reserved word.
+
+Accordingly it was made a reserved word at the immediately following ARG
+meeting.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, July 8, 2010  3:04 PM
+
+Ah, thanks for the info.  I was looking at the latest online version of the AI,
+which has not been updated since the recent meeting.
+
+I'm not surprised by this change.  During Ada 9X, we proposed to have
+nonreserved keywords, and some folks were rabidly opposed to the concept. I seem
+to recall Robert Dewar was one of those.  Either I'm misremembering, or he has
+changed his mind, because he's OK with it now.
+
+I don't really get it -- it seems to me the very practical concern of
+compatibility ought to trump some minor aesthetic unease about the concept of
+nonreserved keywords.  And using Until as a variable name doesn't cause any real
+confusion with "delay until 1.0;" -- no more than using Queue as a user-defined
+type, now that Queue is a predefined type.
+
+****************************************************************
+
+From: Stephen Michell
+Sent: Thursday, July 8, 2010  3:20 PM
+
+Agreed. "some" is now a reserved word.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, July 9, 2010  12:55 PM
+
+> I'm not surprised by this change.  During Ada 9X, we proposed to have
+> nonreserved keywords, and some folks were rabidly opposed to the
+> concept.
+> I seem to recall Robert Dewar was one of those.  Either I'm
+> misremembering, or he has changed his mind, because he's OK with it
+> now.
+
+We also tried it with "interface" for Ada 2005, because of the conflict with
+pragma Interface. That was also rejected. So we're 0-3 on this one.
+
+> I don't really get it -- it seems to me the very practical concern of
+> compatibility ought to trump some minor aesthetic unease about the
+> concept of nonreserved keywords. And using Until as a variable name
+> doesn't cause any real confusion with "delay until 1.0;" -- no more
+> than using Queue as a user-defined type, now that Queue is a
+> predefined type.
+
+Well, WG 9 votes by countries. The US delegation (which is a significant
+fraction of the ARG) was strongly in favor of unreserved keywords. All of the
+rest of the world voted against them (I don't think the feeling was as strong
+for most countries, but it was for a few). That's why this continually comes up:
+this the rare case where by-country voting (as in WG 9) and pluralities (as in
+the ARG) get different answers. To change this result, some of us need to move
+to Canada or France. ;-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, July 9, 2010  1:02 PM
+
+> I seem to recall Robert Dewar was one of those.  Either I'm
+> misremembering, or he has changed his mind, because he's OK with it
+> now.
+
+I am never rapidly against anything, frankly I wuld prefer this time around to
+make SOME non-reserved, since I dislike gratuitous incoimpatibilities, but it's
+not a big deal either way. I am happy to make it reserved.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, July 9, 2010  1:30 PM
+
+> I am never rapidly against anything, ...
+
+Maybe you used the word "rubbish" during the argument -- I don't remember.  ;-)
+
+Interesting typo, by the way.
+
+>...frankly I wuld prefer
+> this time around to make SOME non-reserved, since I dislike
+>gratuitous incoimpatibilities, but it's not a big deal either  way. I
+>am happy to make it reserved.
+
+Yes, I agree 100% with all that.  I'd say the same about "interface"
+and "until".
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, July 9, 2010  1:50 PM
+
+>> I am never rapidly against anything, ...
+>
+> Maybe you used the word "rubbish" during the argument -- I don't
+> remember.  ;-)
+
+rabid seems to be about being angry or emotional, when I call something rubbish,
+it conveys neither, just technical disapproval.
+
+> Interesting typo, by the way.
+>
+>> ...frankly I wuld prefer
+>> this time around to make SOME non-reserved, since I dislike
+>> gratuitous incoimpatibilities, but it's not a big deal either way. I
+>> am happy to make it reserved.
+>
+> Yes, I agree 100% with all that.  I'd say the same about "interface"
+> and "until".
+
+Oh well! The ARG-WG9 community is not attuned enough to the pain of non-upwards
+compatibility, they seem to think that any source in the world can be fed
+through SED :-)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, July 9, 2010  2:31 PM
+
+> rabid seems to be about being angry or emotional, when I call
+> something rubbish, it conveys neither, just technical disapproval.
+
+I'm not sure if you took "rabid" as an insult or not, but just in case you did,
+I apologize!
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, July 9, 2010  3:11 PM
+
+It is impossible to insult me in a technical argument, I never get emotional
+over technical stuff, it is too unimportant for that :-) I like energetic
+argument, but it's never quarrelling for me :-) So, no need to apologize.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Wednesday, July 7, 2010  6:06 AM
+
+I'd like to emphasize the need for cursor ranges for expressing quantified
+properties over containers, in particular for "loop invariants" (even if Ada
+does not define such a notion) on loops which iterate over containers.
+
+Say a loop iterates over a set to increment its values:
+
+   Cont : Set;
+   Cur  : Cursor := First (Cont);
+begin
+   while Has_Element (Cur) loop
+      pragma Assert (for all X in Cont range First (Cont) .. Previous (Cur) |
+                       X = X'Old + 1);
+      pragma Assert (for all X in Cont range Cur .. Last (Cont) |
+                       X = X'Old);
+      Replace_Element (Cont, Cur, Element (Cur) + 1);
+   end loop;
+
+I have written in assertions the loop invariant property of this loop, namely
+that all previous elements have been incremented and all following elements are
+the same.
+
+With ordered sets, it would be possible to express the same properties with
+comparisons between cursors, but then X is not a cursor, plus it would not be
+possible with hashed sets since they don't define comparison between cursors.
+
+Do you see an alternative way of expressing the same properties?
+If not, does it seem reasonable to include ranges over container cursors?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, July 7, 2010  11:03 AM
+
+> I'd like to emphasize the need for cursor ranges for expressing
+> quantified properties over containers, in particular for "loop
+> invariants" (even if Ada does not define such a notion) on loops which
+> iterate over containers.
+
+Keep in mind that there are two forms of iterators for use with containers, one
+using an explicit cursor and one just providing the elements. If you need to
+have a cursor for some reason (including to write Asserts), I think it is
+reasonable to require using the first form. The element form is just a shorthand
+anyway, and is never necessary.
+
+To write your example as a for loop (or as quantified expression), use the
+cursor form:
+
+    for Cur in Iterator(Cont) loop
+      pragma Assert (for all X in Cont range First (Cont) .. Previous (Cur)
+|
+                       X = X'Old + 1);
+      pragma Assert (for all X in Cont range Cur .. Last (Cont) |
+                       X = X'Old);
+      Replace_Element (Cont, Cur, Element (Cur) + 1);
+   end loop;
+
+...
+> With ordered sets, it would be possible to express the same properties
+> with comparisons between cursors, but then X is not a cursor, plus it
+> would not be possible with hashed sets since they don't define
+> comparison between cursors.
+
+It doesn't make sense to talk about a "range" in the hashed containers. What
+would it mean? The order of the elements depends on the hash function and the
+size of the hash table and the implementation and thus is essentially
+unpredictable. It only makes sense to iterate on the entire set of elements for
+one of the hashed forms.
+
+For the other forms, there probably will be ranged iterators available:
+
+    for Cur in Range_Iterator (Cont, Start => First, Finish => Last) loop
+       ...
+
+which of course will just iterate part of the container. The advantage to the
+full form of iterators is that since they are returned by a function, that
+function can have as many parameters as necessary to define the iteration.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Thursday, July 8, 2010  2:07 AM
+
+> Keep in mind that there are two forms of iterators for use with
+> containers, one using an explicit cursor and one just providing the
+> elements. If you need to have a cursor for some reason (including to
+> write Asserts), I think it is reasonable to require using the first
+> form. The element form is just a shorthand anyway, and is never necessary.
+...
+
+The problem I mentioned was about the quantification in the assertion, which is
+always over elements of the container, not cursors, as currently described in
+AI05-0176-1. So you cannot write:
+
+      pragma Assert (for all X in Cont |
+                       if First (Cont) <= X and X <= Previous (Cur)
+                       then X = X'Old + 1);
+
+And since ranges over cursors are not allowed either:
+
+      pragma Assert (for all X in Cont range First (Cont) .. Previous (Cur) |
+                       X = X'Old + 1);
+
+then, there is no way apparently to express the property "all elements before
+the cursor Cur have been incremented".
+
+> It doesn't make sense to talk about a "range" in the hashed
+> containers. What would it mean? The order of the elements depends on
+> the hash function and the size of the hash table and the
+> implementation and thus is essentially unpredictable. It only makes
+> sense to iterate on the entire set of elements for one of the hashed forms.
+
+Right, but during iteration you still have "those elements which have been
+processed" and "those elements which have not", which correspond to the cursors
+"before" and "following" the current cursor. How do you express the property
+above ("all elements before the cursor Cur have been incremented") when
+iterating over a hashed set?
+
+> For the other forms, there probably will be ranged iterators available:
+>
+>     for Cur in Range_Iterator (Cont, Start => First, Finish => Last) loop
+>        ...
+>
+> which of course will just iterate part of the container. The advantage
+> to the full form of iterators is that since they are returned by a
+> function, that function can have as many parameters as necessary to
+> define the iteration.
+
+Interesting, but this only applies to loops, right? What about quantification on
+containers in expressions, as described by AI05-0176-1?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, July 9, 2010  12:47 PM
+
+> The problem I mentioned was about the quantification in the assertion,
+> which is always over elements of the container, not cursors, as
+> currently described in AI05-0176-1. So you cannot write:
+>
+>       pragma Assert (for all X in Cont |
+>                        if First (Cont) <= X and X <= Previous (Cur)
+>                        then X = X'Old + 1);
+
+I had thought the intent was that all of the iterator forms would be supported
+in quantified expressions, but it is clear that the current AI does not do that.
+I think you have demonstrated why the cursor forms are needed in quantified
+expressions, so we ought to revisit that.
+
+> > It doesn't make sense to talk about a "range" in the hashed
+> > containers. What would it mean? The order of the elements depends on
+> > the hash function and the size of the hash table and the
+> > implementation and thus is essentially unpredictable. It only makes
+> > sense to iterate on the entire set of elements for one of
+> the hashed forms.
+>
+> Right, but during iteration you still have "those elements which have
+> been processed" and "those elements which have not", which correspond
+> to the cursors "before" and "following" the current cursor. How do you
+> express the property above ("all elements before the cursor Cur have
+> been
+> incremented") when iterating over a hashed set?
+
+I don't think you can, and I'm not sure it makes sense to do so. Cursors in a
+hashed set have no order, and there is no reason to assume that the order
+selected for a particular iterator can even be reproduced (a later iterator may
+use a different order). Any dependence on ordering is bogus.
+
+Why don't you just check that all of the elements are processed after the loop
+completes? It would be cheaper (the check you propose is quadratic) and would
+have the same effect.
+
+...
+> Interesting, but this only applies to loops, right? What about
+> quantification on containers in expressions, as described by
+> AI05-0176-1?
+
+Quantifiers need the cursor forms, for this reason and the others you noted.
+That ought to be fixed. After all, the cursor forms are the more general ones,
+and limiting only to the less general forms always is going to lead to trouble.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, July 9, 2010  1:25 PM
+
+> Why don't you just check that all of the elements are processed after
+> the loop completes? It would be cheaper (the check you propose is
+> quadratic) and would have the same effect.
+
+I suspect Yannick is thinking about static proofs here.
+
+Yeah, you'd have an assertion after the loop (or a postcondition on the
+procedure).  You're trying to deduce that that's True, from the loop invariant
+("all the ones done so far have so-and-so property"), plus the exit condition
+("the ones done so far = all of them"). And you deduce the loop invariant
+inductively (if it was True last time around, then it must be True this time).
+
+This sort of reasoning doesn't care that hash tables iterate in an arbitrary
+order.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, July 9, 2010  1:49 PM
+
+Right, but it does require that the order to reproducible, and there is no such
+requirement on the hashed containers at this point. The only requirement is that
+each item is touched only once for a particular iterator instance. A perfectly
+acceptable implementation would have a list of items yet to be processed stored
+as part of the iterator; the container itself may not have any knowledge of the
+order of operations and surely will not know the state of the iterator (iterator
+objects being separate from the container for the new iterators, and the
+information being stored in the locals of the subprogram for the existing
+passive iterators). In order to say anything about the order (such as having
+functions to query whether or not an item is already processed), the container
+has to know the order and keep it unchanged so long as any one can reasonably
+ask about it. That seems like a significant impact on the design of what is
+supposed to be an unordered container.
+
+I would think that static proofs for unordered iterators have to be done on the
+loop as a whole (not on intermediate positions). That is, there has to be a
+proof that all of the iterations complete (no exceptions raised, etc.) and that
+each iteration has the intended effect on its single element. I realize that's
+easier said than done. But the sort of loop invariants that Yannick is talking
+about don't make sense in the absence of a defined order, and aren't really
+necessary for whole container iterators unless there is an intent that the loop
+not complete all of the iterations. That is, if the intent is that the loop
+operate on the entire container without interruption, there is no need to have
+loop invariants that say anything about elements other than the current one.
+(That job ought to be done by an assertion or the like after the loop.)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, July 9, 2010  2:28 PM
+
+> Right, but it does require that the order to reproducible, and there
+> is no such requirement on the hashed containers at this point.
+
+Good point -- I didn't think of that!
+
+Perhaps there should be.  That is, if you iterate twice over the same container,
+and it hasn't changed, then the iterations happen in the same order (but that
+order is arbitrary). By "change", I mean adding/inserting/moving elements --
+modifying the content of elements doesn't count.
+
+I can't imagine any sensible implementation of hash tables that would violate
+this rule, and it seems somewhat useful.
+
+If you insert an element into the hash table, that can of course radically alter
+the order of subsequenct iterations.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, July 9, 2010  2:42 PM
+
+All of the iterator forms should be included in the quantified expr. This was
+probably just an oversight.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Monday, July 12, 2010  2:41 AM
+
+>> Right, but it does require that the order to reproducible, and there
+>> is no such requirement on the hashed containers at this point.
+>
+> Good point -- I didn't think of that!
+>
+> Perhaps there should be.  That is, if you iterate twice over the same
+> container, and it hasn't changed, then the iterations happen in the
+> same order (but that order is arbitrary).
+> By "change", I mean adding/inserting/moving elements -- modifying the
+> content of elements doesn't count.
+
+That would be terribly useful for static verification.
+
+As you correctly guessed in a previous email, I am concerned with the ability to
+express loop invariants for static verification. These are properties that are
+maintained throughout the loop and which usually describe the intermediate state
+of the container during iteration. So there must be a way to describe those
+elements which have been treated and those elements which have not.
+
+It is not sufficient to describe the result of the loop after a complete
+execution: it will be possible to test it during execution, but this will not be
+provable statically without a loop invariant as described above.
+
+> I can't imagine any sensible implementation of hash tables that would
+> violate this rule, and it seems somewhat useful.
+
+In order to have properties that are used both for dynamic and static
+verification, this is very useful.
+
+> If you insert an element into the hash table, that can of course
+> radically alter the order of subsequenct iterations.
+
+agreed, no problem with that.
+
+****************************************************************
+
+From: Randy Brukardy
+Sent: Monday, July 26, 2010  9:12 PM
+
+> All of the iterator forms should be included in the
+> quantified expr. This was probably just an oversight.
+
+For the record, I've fixed up the draft version of AI05-0176-1 to reference all
+of the new syntax proposed in AI05-0139-2. I believe that will be sufficient to
+include all of the iterator forms.
 
 ****************************************************************
 

Questions? Ask the ACAA Technical Agent