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

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

--- ai05s/ai05-0176-1.txt	2010/02/04 03:46:40	1.3
+++ ai05s/ai05-0176-1.txt	2010/02/04 07:11:43	1.4
@@ -1,4 +1,4 @@
-!standard 2.9(2/2)                                  10-02-03  AI05-0176-1/02
+!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)
@@ -102,41 +102,48 @@
      the subtype of the quantified expression parameter is the element type of
      the container.
 
-   Name resolution rules
+   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.
 
-   Dynamic semantics
+A predicate is expected to be of any boolean 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
+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
+* If the quantifier is "for all" the expression is True if 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
+  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'Pred(A'Last) | A (I) <= A(I'Succ))
 
-  Post =>  (for all I in A'First .. A'Last'Pred | A (I) <= A(I'Succ))
+[Editor's note: What is I'Succ here? 'Succ isn't defined on objects. It
+probably ought to be something like Index_Subtype'Succ(I), but I didn't change
+it because I don't know the type of I. (I did change "A'Last'Pred" to the
+correct A'Pred(A'Last)).]
 
 !discussion
 
@@ -1461,3 +1468,40 @@
 
 ****************************************************************
 
+From: Ed Schonberg
+Sent: Wednesday, February 3, 2010  9:43 PM
+
+>                     Randy, overworked editor.
+
+Thanks for the careful editing. I'll check about the presence of Exists
+in our sources.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, February 3, 2010  10:42 PM
+
+For the record, I realized that I had forgotten to actually read most of it (I
+was focused on typos). When I went back and did that, I found more typos that I
+fixed, and also that you forgot to define the expected type of a "predicate". I
+fixed the latter by copying the wording for "condition".
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, February 3, 2010  10:31 PM
+
+How about "(for'all X in ...)" and "(for'some X in ...)"?
+Or "(for-all X in ...)" and "(for-some X in ...)"?
+Both of these would allow "some" not to be a reserved word.  I agree with Randy
+that "Exists" is simply too common of a name for functions.  I know I have
+written "if Exists(X) then ..." many times in various Ada applications.  We
+either need a way to have an unreserved keyword, or pick some other less common
+word.
+
+In terms of less common words to make reserved, we could use "for_all" and
+"there_exists":
+
+   (for_all X in ...) and (there_exists X in ...)
+
+****************************************************************

Questions? Ask the ACAA Technical Agent