--- 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