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

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

--- ai05s/ai05-0176-1.txt	2009/11/04 06:28:31	1.2
+++ ai05s/ai05-0176-1.txt	2010/02/04 03:46:40	1.3
@@ -1,4 +1,7 @@
-!standard 4.5.1                                  09-10-28  AI05-0176-1/01
+!standard 2.9(2/2)                                  10-02-03  AI05-0176-1/02
+!standard 3.3(19)
+!standard 4.4(7)
+!standard 4.5.9(0)
 !class Amendment 09-10-28
 !status work item 09-10-28
 !status received 09-10-28
@@ -13,26 +16,33 @@
 
 !problem
 
-It is very common in formal developement to define a predicate over a collection
+It is very common in formal development to define a predicate over a collection
 to express the fact that all elements of the collection satisfy a given
-property. (This is of course borrowed from the language of set theory and fornal
-logic). For example, the fact that an array A is sorted can be expressed by
-stating that for all values of an index I in the range from A'First to A'Last -
-1 inclusive, the property A(I) <= A (I+1) obtains. Mathematical usage is to
-write, e.g.  forall X | P (X),  to indicate that all elemnts X satisfy the
-property P (X). When using such notation, the context is supposed to indicate
-the universe in which the elements X are to be found. This is of course not
-usable in a programming language that is meant to be executable, and the syntax
-must indicate the domain of definition of the element. The common notation is:
-forall X in domain | P (X).
-
-The domain can be a range, or an expression that designates a container. The
-first is typically used when the collection is an array, and the index
-(the bound variable in the expression) is used to denote an element of the
-collection in the condition. For collections with no built-in ordering, the
-bound variable denotes directly an element of the collection:
+property, or that at least one element of the collection satisfies it. (This is
+of course borrowed from the language of set theory and fornal logic). For
+example, the fact that an array A is sorted can be expressed by stating that for
+all values of an index I in the range from A'First to A'Last - 1 inclusive, the
+property A(I) <= A (I+1) obtains. Mathematical usage is to write, e.g.  forall X
+| P (X),  to indicate that all elemnts X satisfy the property P (X). When using
+such notation, the context is supposed to indicate the universe in which the
+elements X are to be found. This is of course not usable in a programming
+language that is meant to be executable, and the syntax must indicate the domain
+of definition of the element. The common notation is:
+
+      forall X in domain | P (X),
+
+Similarly, to indicate that some element of the domain satisfies a given
+property, we write
+
+      exists 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 index (the
+bound variable in the expression) is used to denote an element of the collection
+in the condition. For collections with no built-in ordering, the bound variable
+denotes directly an element of the collection:
 
-        for all X in Directory | Name (X)'Length < 20
+         for all X in Directory | Name (X)'Length < 20
 
 Directory may be one of the predefined containers, or an array.
 
@@ -40,6 +50,11 @@
 
 !proposal
 
+Introduce quantified expressions in the language, with their usual meaning:
+boolean expressions that verify whether all (resp. al least one) element in a
+collection (array or container) satisfies a given predicate. Introduce a new
+keyword: "exists" to support this feature.
+
 Quantified expressions have the following syntax:
 
    ( for all defining_identifier in Domain | Boolean_Expression )
@@ -47,9 +62,82 @@
    Domain =>  Discrete_Range | Expression
 
 !wording
+
+Add in 2.9 a new reversed word
+   exists
+
+Modify 3.3 (19):
+
+   * a loop parameter, choice parameter, quantified expression parameter,
+     or entry index;
+
+Add to 4.4 (7) a new kind of primary:
+   quantified_expression
+
+Add a new clause (after the proposed clauses for conditional expressions
+(AI05-0147) and case expressions (AI05-0188-1):
+
+4.5.9 Quantified expressions
+
+   quantified_expression ::=
+     (quantifier defining_identifier in domain | predicate)
+
+   quantifier ::=  for all | exists
+
+   domain ::=  discrete_subtype_definition | expression
+   predicate ::= boolean_expression
+
+   Static Semantics
+
+A quantified expression declares a *quantified expression parameter*, whose
+subtype is defined by the domain:
+
+   * if the domain is a discrete_subtype_definition, this is the subtype of the
+     quantified expression parameter.
+
+   * if the domain is an expression that is a one-dimensional array, the subtype
+     of the quantified expression parameter is the element type of the array.
+
+   * if the domain is an expression whose value is an instance of a container,
+     the subtype of the quantified expression parameter is the element type of
+     the container.
+
+   Name resolution rules
+
+The expected type of a quantified expression is the predefined type Boolean.
+
+If the domain is an expression, it is expected to be of any type.
 
-<tbd>
+   Dynamic semantics
 
+The evaluation of a quantified expression assigns to the quantified expression
+parameter each one of the values specified by the domain, If the domain is a
+range, those values are assigned in order. In the domain is an array, the values
+are assigned in order of increasing index. If the domain is a container, the
+values are assigned in the order in which container elements are examined in an
+iteration over the container, using the primitives First and  Next. The
+predicate is then evaluated for each value of the quantified
+expression parameter. The value of the quantified expression is determined as
+follows:
+
+* If the quantifier is "for all" the expression is True is the evaluation of the
+  predicate yields True for each value of the quantified_expression parameter.
+  It is false otherwise. Evaluation of the expression stops when all values of
+  the domain have been examined, or when the predicate yields False for a given
+  value.
+
+* If the quantifier is "exists" the expression is True is the evaluation of the
+  predicate yields True for some value of the quantified_expression_parameter.
+  It is false otherwise. Evaluation of the expression stops when all values of
+  the domain have been examined, or when the predicate yields True for a given
+  value.
+
+Examples
+
+The postcondition for a sorting routine on arrays can be written:
+
+  Post =>  (for all I in A'First .. A'Last'Pred | A (I) <= A(I'Succ))
+
 !discussion
 
 Instead of a vertical bar, we could use a colon to separate the iterator from
@@ -58,6 +146,24 @@
 When quantifying over an array, the syntax provides the index, i.e. a cursor
 over the array. There is no obvious domain over which to define a cursor in the
 case of a container, so the notation  (for all X in C | P (X)) is natural.
+However, for the case of Maps, it would be attractive to have a form that binds
+both a key and the corresponding element in the container. This suggests
+introducing an attribute 'Domain  (we already have 'Range) so we could write
+
+     (for all Key in M'Domain ( Find (M, Key) > 7)
+
+Given that a mapping has a domain and a range, this suggests generalizing both
+of these attributes to be used in quantified expressions and in loops, but this
+is probably too big a change at this time.
+
+!discussion
+
+Instead of a vertical bar, we could use a colon to separate the iterator from
+the condition. The proposed notation is more common in mathematics.
+
+When quantifying over an array, the syntax provides the index, i.e. a cursor
+over the array. There is no obvious domain over which to define a cursor in the
+case of a container, so the notation  (for all X in C | P (X)) is natural.
 However, for the case of Maps, it would be attractive to have a form that
 binds both a key and the corresponding element in the container. This suggests
 introducing an attribute 'Domain  (we already have 'Range) so we could write
@@ -70,9 +176,9 @@
 
 !example
 
-** TBD **
+(See wording.)
 
---!corrigendum 4.5.1(0)
+--!corrigendum 4.5.9(0)
 
 
 !ACATS test
@@ -755,3 +861,603 @@
 type of the thing you are manipulating.
 
 ****************************************************************
+
+From: Bob Duff
+Sent: Monday, November 16, 2009  10:54 PM
+
+AI05-0176-1, Quantified expressions was mentioned recently.
+
+I think we should have an e-mail discussion of this issue, which was raised by
+John Barnes at the recent meeting:
+
+If we're going to have the universal quantifier "for all", we ought to also have
+the existential quantifier.  John suggested the syntax "for some", which I like.
+
+It looks pretty silly to have one without the other -- reading the double
+negative (not (for all... (not...))) is pretty ugly.  Sort of like having "and
+then" but not "or else" in the language.
+
+Are we willing to tolerate the new reserved word "some"?
+
+I'm not sure where I stand, but I'm in kind of a "both or neither" mood right
+now.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, November 16, 2009  5:11 PM
+
+The other possibility is of course exists. How about we do a run on the GNAT
+test suite to see how much use of either identifier there is. I will post
+results on this ASAP.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, November 16, 2009  5:36 PM
+
+Good idea.
+
+FWIW, "for some" reads nicely to me.  I'm not sure whether you're suggesting
+"for exists" or "if exists".  To me, "for exists" looks weird.  But I don't like
+"if exists" either, because it's a loop, so should have "for".
+
+I shall refrain from suggesting a backwards E, which I guess exists (heh heh)
+somewhere in Unicode.  ;-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, November 16, 2009  5:46 PM
+
+to me it is fine to write
+
+     if for all ...
+
+     if exists
+
+really the first line should be
+
+     if forall ...
+
+and really we should allow the special symbols (gosh, we have them available in
+the 32-bit character set I am sure :-) :-) :-)
+
+     while for some ...
+
+seems less nice to me than
+
+     while exists
+
+but then I am biased by having programmed using while exists and while forall
+for many decades.
+
+> I shall refrain from suggesting a backwards E, which I guess exists
+> (heh heh) somewhere in Unicode.  ;-)
+
+Well as per above, you are only allowed to suggest this if you suggest the
+corresponding symbol for FORALL :-)
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, November 16, 2009  5:49 PM
+
+"exists"  stands by itself to define a quantified expression:       if
+exists X in S: ....     or    while exists X in S: ....
+
+I find it slightly preferable to  "for some"
+
+****************************************************************
+
+From: Gary Dismukes
+Sent: Monday, November 16, 2009  5:49 PM
+
+> FWIW, "for some" reads nicely to me.  I'm not sure whether you're
+> suggesting "for exists" or "if exists".  To me, "for exists" looks
+> weird.  But I don't like "if exists" either, because it's a loop, so should
+> have "for".
+
+I suspect that 'some' is very rare, whereas I can easily imagine there are
+programs using 'exists' (as a predicate function name).
+
+> I shall refrain from suggesting a backwards E, which I guess exists
+> (heh heh) somewhere in Unicode.  ;-)
+
+;-)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, November 16, 2009  7:09 PM
+
+Actually, we do have the mathematical symbols to draw on. Pi got its nose in the
+tent for Ada 2005, Perhaps we could adopt ? and ? directly.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, November 16, 2009  7:12 PM
+
+Edmond Schonberg wrote:
+
+> "exists"  stands by itself to define a quantified expression:       if
+> exists X in S: ....     or    while exists X in S: ....
+>
+> I find it slightly preferable to  "for some"
+
+Ed, your comment, and Robert's similar comment, seem somewhat convincing to me,
+but I think I need to see the full BNF syntax before I can really "see" it.
+
+Gary's comment:
+
+> I suspect that 'some' is very rare, whereas I can easily imagine there
+> are programs using 'exists' (as a predicate function name).
+
+is a strong argument for 'some', but let's see the result of Robert's experiment
+first.
+
+> > I shall refrain from suggesting a backwards E, which I guess exists
+> > (heh heh) somewhere in Unicode.  ;-)
+>
+> Well as per above, you are only allowed to suggest this if you suggest
+> the corresponding symbol for FORALL :-)
+
+Yes, of course.  ;-)  I shall also refrain from suggesting an upside-down A.
+I couldn't type an upside-down A on my keyboard to save my life!
+
+My opinion: You shouldn't have to know any more than 4'th grade math to learn
+how to program.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, November 16, 2009  8:59 PM
+
+> Actually, we do have the mathematical symbols to draw on. Pi got its
+> nose in the tent for Ada 2005,
+
+That was a mistake, IMHO.
+
+> Perhaps we could adopt ? and ? directly.
+
+Cool!  Those look like upside-down A and backwards E on my screen!  I've no idea how you typed them in.
+
+I hope you're kidding, Tuck.  We really don't want the predefined stuff to
+depend on anything but 7-bit ASCII.  It's fine to allow another 2**N characters,
+for N=31 or whatever, but let's not put that in the predefined stuff.
+
+P.S. Actually, that upside-down A has an extra serif on the side that looks
+weird to me.  And probably looks weird to Donald Knuth.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, November 16, 2009  9:16 PM
+
+> > Actually, we do have the mathematical symbols to draw on. Pi got its
+> > nose in the tent for Ada 2005,
+>
+> That was a mistake, IMHO.
+
+That's just an identifier, and there is an ASCII equivalent. Any user could have
+done the same.
+
+> > Perhaps we could adopt ? and ? directly.
+>
+> Cool!  Those look like upside-down A and backwards E on my screen!
+> I've no idea how you typed them in.
+
+On my screen, I just see ? and ?. Not very helpful. (I'd type them in opening
+the symbol page in OpenOffice or Word, inserting them into a blank document, and
+then cut-and-pasting them into my e-mail. Not fun. Probably a programming editor
+would have a similar page, so it wouldn't be quite that bad in practice.) In any
+case, I have to remove characters like that from the filed mail, or I get
+complaints about "garbage" in the files. So please minimize the use of them
+here.
+
+> I hope you're kidding, Tuck.  We really don't want the predefined
+> stuff to depend on anything but 7-bit ASCII.  It's fine to allow
+> another 2**N characters, for N=31 or whatever, but let's not put that
+> in the predefined stuff.
+
+I wouldn't object if they were identifiers and there were regular ASCII
+representations available as well. (As in the PI case.) But to use them *in
+place* of reserved words is really nasty. So I too hope Tucker was kidding.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, November 16, 2009  9:44 PM
+
+>> Perhaps we could adopt ? and ? directly.
+>
+> Cool!  Those look like upside-down A and backwards E on my screen!
+> I've no idea how you typed them in.
+
+The joys of using a Mac (and UTF-8).  ;-)
+
+...
+> P.S. Actually, that upside-down A has an extra serif on the side that
+> looks weird to me.  And probably looks weird to Donald Knuth.
+
+The pain of infinite font choices. ;-(
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, November 16, 2009  11:52 PM
+
+> > Cool!  Those look like upside-down A and backwards E on my screen!
+> > I've no idea how you typed them in.
+>
+> The joys of using a Mac (and UTF-8).  ;-)
+
+For what it's worth (probably $0.00 :-), neither of those characters appear in
+the "special symbols" page of OpenOffice for the fonts provided with Windows XP.
+I believe OpenOffice shows all of the characters defined in the fonts (it is
+around a thousand characters for Times New Roman, including a lengthy set of
+Arabic characters -- but only a handful of math characters); it is nice enough
+to show the (Unicode) encoding of the characters. I suppose its possible that I
+looked in the wrong place; what codes are those characters??
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, November 16, 2009  11:59 PM
+
+Following up, I found these in the Symbol font, with character codes F022 and
+F024; those codes are in the "private use area" and doesn't have the same glyphs
+in other fonts. So I'm pretty sure that typical Windows fonts don't have those
+characters. Which suggests against using them (having to use a special font to
+display them is obnoxious at best). (Haven't checked Windows 7 yet, perhaps it
+has more characters.)
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Tuesday, November 17, 2009  4:09 AM
+
+> "exists"  stands by itself to define a quantified expression:       if
+> exists X in S: ....     or    while exists X in S: ....
+>
+> I find it slightly preferable to  "for some"
+>
+So do I - but of course I am part of the gang under SETL influence ;-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, November 17, 2009  6:34 AM
+
+> Actually, we do have the mathematical symbols to draw on. Pi got its
+> nose in the tent for Ada 2005, Perhaps we could adopt ∀ and ∃
+> directly.
+
+Tee hee, someone rose to the bait!
+
+The introduction of Pi in the library was a HUGE pain, it required all sorts of special fiddling for us to deal with.
+I really don't want to get into this for the language itself.
+We could possibly allow these as alternatives, but you don't want to insist on
+them. In many environments this would simply make the features unavailable.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, November 17, 2009  6:36 AM
+
+>> I suspect that 'some' is very rare, whereas I can easily imagine
+>> there are programs using 'exists' (as a predicate function name).
+>
+> is a strong argument for 'some', but let's see the result of Robert's
+> experiment first.
+
+I don't think "I suspect" can ever be a "strong argument". Indeed let's wait for
+the result of the experiment.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, November 17, 2009  6:37 AM
+
+> Cool!  Those look like upside-down A and backwards E on my screen!
+> I've no idea how you typed them in.
+
+not on my screen :-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, November 17, 2009  6:38 AM
+
+> That's just an identifier, and there is an ASCII equivalent. Any user
+> could have done the same.
+
+NOT!
+
+They could not have done it in the standard library, and it has been a HUGE pain
+for us to accomodate this one special case.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, November 17, 2009  8:20 AM
+
+> > Cool!  Those look like upside-down A and backwards E on my screen!
+> > I've no idea how you typed them in.
+>
+> not on my screen :-)
+
+Now you've mailed them back to me, they look different.
+The for-all symbol looks like an 'a' with a '^' on top, followed by a '^',
+followed by a Euro symbol (three characters).
+
+And when Randy mailed them back to me, they both looked like '?'.
+
+Q.E.D. (that we shouldn't touch such characters with a barge pole)
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Tuesday, November 17, 2009  3:19 AM
+
+RE: "for some" vs. "exists"....
+
+Is this a contest at all? Is there anybody who prefers "for some" to "exists"?
+(in boolean expressions)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, November 17, 2009  11:52 AM
+
+I think I prefer "for some" because it better suggests the loop involved.  I am
+also somewhat swayed by the fact that "exists" will never fly as a reserved
+word, whereas I could imagine handling "for some" either by making "some"
+reserved, or by only reserving it in this context.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, November 17, 2009  12:00 PM
+
+Same here.  Also, I don't see any need to be overly mathematical in our
+notation.  (E.g. I much prefer using the words "and" and "or" over the operators
+maths folks sometimes use -- even if those operators were part of 7-bit ascii
+and appeared on my keyboard.)
+
+But I'm not sure, because I haven't seen the exact BNF being proposed for
+'exists'.
+
+By the way, some people are fanatically opposed to semi-reserved keywords.  Not
+me.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, November 17, 2009  12:06 PM
+
+> Is this a contest at all? Is there anybody who prefers "for some" to
+> "exists"? (in boolean expressions)
+
+I don't like either much. Moreover, "Exists" does not fly as a reserved word for
+me. I found a number of instances of parameters and variables named "Exists" in
+part of the Janus/Ada compiler (a small sample, but I think it is instructive):
+
+
+    procedure Task_Guard(Exists : in Boolean);
+
+---
+
+    procedure Find_SYM (Current_Class : in out J2Typ_Decs.Library_Type;
+                        Line       : in Target.Line_Numbers;
+                        Pos        : in Target.Line_Position;
+                        Can_Create : in Boolean;
+                        Exists     : out Boolean);
+
+---
+
+            Exists : Boolean;
+                                 Can_Create => FALSE, Exists => Exists);
+            if Exists then
+
+(There are two more instances like this in this package; these are all making
+calls on Find_SYM)
+
+---
+
+Perhaps these would have been better named "File_Exists" or something like that
+(there are a *lot* of those in the Janus/Ada compiler), but I doubt that our
+code is atypical. Thus I think the incompatibility caused by "Exists" as a
+reserved word is unacceptable.
+
+---
+
+I didn't try all of the compiler tools or any of our other code (as I did the
+looking with a simple text search).
+
+I tried a similar search for Some; I didn't find any declarations, but it's hard
+to tell because of the number of comments and larger identifiers containing the
+text "Some". We need a smarter tool for that. Presumably, the AdaCore experiment
+will give a more definitive answer.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, November 17, 2009  12:09 PM
+
+> By the way, some people are fanatically opposed to semi-reserved
+> keywords.  Not me.
+
+Not me either, but I don't like to allow them unless they appear in a position
+where the identifier could not occur reading left to right
+
+     for some in x .. y loop
+
+     for some x ...     loop
+
+seems uncomfortable to me
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, November 17, 2009  12:10 PM
+
+Note that if you tolerate semi-reserved keywords, exists is fine because you
+will always have an identifier after exists
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Wednesday, November 18, 2009  1:48 AM
+
+> I tried a similar search for Some; I didn't find any declarations, but
+> it's hard to tell because of the number of comments and larger
+> identifiers containing the text "Some". We need a smarter tool for that.
+:-) Adacontrol's rule:
+check entities (all some, all exists);
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Wednesday, February 3, 2010  5:21 PM
+
+here is a more fleshed-out proposal.  It may still depend on the new iterator
+machinery, but most of it stands on its own.  I think we have to bite the bullet
+and introduce the keyword "exists".
+
+[This is version /02 - Editor.]
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, February 3, 2010  5:21 PM
+
+> here is a more fleshed-out proposal.  It may still depend on the new
+> iterator machinery, but most of it stands on its own.
+>  I think we have to bite the bullet and introduce the keyword
+> "exists".
+
+That's a huge bullet. When we discussed this back in November, I did a quicky
+look at the code of a portion of Janus/Ada (about 25%) and found more than 20
+parameters and objects named "Exists". I just did a look at the public part of
+Claw and found 4 overloaded functions named "Exists".
+
+Robert was going to look at this in the AdaCore test suite, but he never
+reported back. But in the absence of him reporting that our code here is
+unusual, I would have to be 100% against making "exists" a reserved word.
+Especially for something that I would use rarely.
+
+...
+> !wording
+> Add in 2,9 a new keyword
+>    exists
+
+2.9 defines "reserved words", not "keywords" (that was the name of the
+unreserved identifiers that we dropped last time after substantial opposition).
+I've corrected this.
+
+> Add to 3.3 (19) a new constant
+>       quantified_expression_parameter
+
+This is written as a syntax item, but in the grammar you give below, this is not
+defined. And in the for loop wording that you presumably are borrowing from,
+this is a defined term, not a syntax. I've fixed this consistently throughout
+the proposal.
+
+> 4.5.8 Quantified expressions
+
+The clause number needs to be 4.5.9, at least given the existing other AIs.
+Maybe we'll change that in the future.
+
+>    quantified_expression ::=
+>     (quantifier defining_identifier in domain | predicate)
+>
+>       quantifier ::=  for all | exists
+>
+>      domain ::=  discrete_subtype_definition | expression
+>      predicate ::= boolean_expression
+
+I don't get why these things are indented randomly. The indentation of Ada
+syntax is significant. I made them all consistent, but you need to tell me if
+that is what you meant.
+
+>    Static Semantics
+>
+> A quantified expression declares a
+> quantified_expression_parameter, whose subtype is defined by the
+> domain:
+
+This is a term, no underscores, and, as this is the defining occurrence, it
+needs to be surrounded by *stars*.
+
+>    if the domain is a discrete_subtype_definition, this is the subtype
+> of the
+>     quantified_expression_parameter.
+>
+>    if the domain is an expression that is a one-dimensional array, the
+> subtype
+>    of the quantified_expression_parameter is the element type of the
+> array
+>
+>    if the domain is an expression whose value is an instance of a
+> container,
+>     the subtype of the quantified_expression_parameter is the element
+> type of
+>     the container.
+
+I think this is supposed to be a bulleted list, but there is no bullets to be
+seen. And the second one seems to have a punctuation shortage.
+
+>    Name resolution rules
+>
+> The expected type of a quantified expression is the predefined type
+> Boolean
+
+More missing punctuation.
+
+>    If the domain is an expression, it is expected to be of any type.
+>
+> Dynamic semantics
+>
+> The evaluation of a quantified expression assigns to the
+> quantified_expression_ parameter each one of the values specified by
+> the domain, If the domain is a range, those values are assigned in
+> order. In the domain is an array, the values are assigned in order of
+> increasing index. If the domain is a container, the values are
+> assigned in the order in which container elements are examined in an
+> iteration over the container, using the primitives First and  Next.
+> The predicate is then evaluated for each value of the quantified_
+> expression_parameter. The value of the quantified expression is
+> determined as
+> follows:
+>
+> If the quantifier is "for all" the expression is True is the
+> evaluation of the predicate yields True for each value of the
+> quantified_expression parameter.
+> It is false otherwise. Evaluation of the expression stops when all
+> values of the domain have been examined, or when the predicate yields
+> False for a given value.
+>
+> If the quantifier is "exists" the expression is True is the evalution
+> of the predicate yields True for some value of the
+> quantified_expression_parameter.
+> It is false otherwise.  Evaluation of the expression stops when all
+> values of the domain have been examined, or when the predicate yields
+> True for a given value.
+
+Another bulleted list?? "Evalution".
+
+...
+> Given that a mapping has a domain and a range, this suggests
+> generalizing both of these attributes to be used in quantified
+> expressions and in loops, but this is probably too big a change at
+> this time.
+>
+> ed:ALL_AI05 schonberg$
+
+This looks like your computer's command line prompt. How did it get in your
+e-mail?
+
+****************************************************************
+

Questions? Ask the ACAA Technical Agent