--- ai05s/ai05-0176-1.txt 2010/05/20 06:38:00 1.12 +++ ai05s/ai05-0176-1.txt 2010/06/04 06:18:22 1.13 @@ -1,7 +1,8 @@ -!standard 1.1.4(12) 10-04-12 AI05-0176-1/06 +!standard 1.1.4(12) 10-06-03 AI05-0176-1/07 !standard 4.4(7) !standard 4.5.9(0) !class Amendment 09-10-28 +!status Amendment 2012 10-06-03 !status ARG Approved 6-1-3 10-02-27 !status work item 09-10-28 !status received 09-10-28 @@ -12,7 +13,7 @@ !summary -Syntax is proposed for quantified expressions over a finite domain. +Syntax is added for quantified expressions over a finite domain. !problem @@ -22,8 +23,8 @@ 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). +A(I) <= A (I+1) holds. Mathematical usage is to write, e.g. forall X | P (X), +to indicate that all elements 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 @@ -56,7 +57,7 @@ !proposal Introduce quantified expressions in the language, with their usual meaning: -boolean expressions that verify whether all (resp. al least one) element in a +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. @@ -84,55 +85,74 @@ 4.5.9 Quantified expressions - quantified_expression ::= (for quantifier loop_parameter_specification | predicate) +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.] +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. + +Wherever the Syntax Rules allow an expression, a quantified_expression may be +used in place of the expression, so long as it is immediately surrounded by +parentheses. + +AARM Discussion: The syntactic category quantified_expression appears only +as a primary that is parenthesized. The above rule allows it to additionally +be used in other contexts where it would be directly surrounded by +parentheses. This is the same rule that is used for conditional_expressions; +see 4.5.7 for a detailed discussion of the meaning and effects of this rule. + Name Resolution Rules -The expected type of a quantified expression is any Boolean type. -The predicate in a quantified_expression is expected to be the same type. +The expected type of a quantified_expression is any Boolean type. +The predicate in a quantified_expression is expected to be of the same type. Dynamic Semantics -For the evaluation of a quantified expression, the loop_parameter_specification -is first elaborated. The evaluation of a quantified expression then evaluates -the predicate for each value of the loop_parameter. These values are examined -in the order specified by the loop_parameter_specification. - -The value of the quantified expression is determined as follows: - -* If the quantifier is "all" the expression is True if the evaluation of the - predicate yields True for each value denoted by the loop_parameter. It is - False otherwise. Evaluation of the quantified expression stops when all values +For the evaluation of a quantified_expression, the loop_parameter_specification +is first elaborated. The evaluation of a quantified_expression then evaluates +the predicate for each value of the loop parameter. These values are examined +in the order specified by the loop_parameter_specification (see 5.5). + +The value of the quantified_expression is determined as follows: + +* If the quantifier is "all", the expression is True if the evaluation of the + predicate yields True for each value of the loop parameter. It is False + otherwise. Evaluation of the quantified_expression stops when all values of the domain have been examined, or when the predicate yields False for a given value. Any exception raised by evaluation of the predicate is propagated. -AARM note: the expression is True if the domain contains no values. +AARM ramification: The expression is True if the domain contains no values. -* If the quantifier is "some" the expression is True is the evaluation of the - predicate yields True for some value of the loop_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. Any - exception raised by evaluation of the predicate is propagated. +* If the quantifier is "some", the expression is True if the evaluation of the + predicate yields True for some value of the loop parameter. It is False + otherwise. Evaluation of the quantified_expression stops when all values + of the domain have been examined, or when the predicate yields True for a + given value. Any exception raised by evaluation of the predicate is + propagated. -AARM note: the expression is False if the domain contains no values. +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 arrays with can be written: +The postcondition for a sorting routine on an array A with an index subtype T can +be written: -Post => (for all I:T in A'First .. T'Pred(A'Last) | A (I) <= A (T'Succ (I))) +Post => (for all I 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: - (for some X in 2 .. N / 2 | N mod X = 0) + pragma Assert (for some X in 2 .. N / 2 | N mod X = 0); -Note: Some is not a reserved word. !discussion @@ -148,13 +168,89 @@ !example (See Wording.) + +!corrigendum 1.1.4(12) + +@drepl +@xbullet<A vertical line separates alternative items unless it immediately occurs +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:> + +!corrigendum 4.4(7) + +@drepl +@xcode<@fa<primary ::=> + @fa<numeric_literal | >@ft<@b<null>>@fa< | string_literal | aggregate> + @fa<| name | qualified_expression | allocator | (expression)>> +@dby +@xcode<@fa<primary ::=> + @fa<numeric_literal | >@ft<@b<null>>@fa< | string_literal | aggregate> + @fa<| name | qualified_expression | allocator | (expression) | (quantified_expression)>> + +!corrigendum 4.5.9(0) + +@dinsc + +@s8<@i<Syntax>> + +@xcode<@fa<quantified_expression ::= >@ft<@b<for>>@fa< quantifier loop_parameter_specification | predicate +quantifier ::= >@ft<@b<all>>@fa< | >@ft<Some>@fa< +predicate ::= >@ft<@i<boolean_>>@fa<expression>> + +Wherever the Syntax Rules allow an @fa<expression>, a @fa<quantified_expression> may be +used in place of the @fa<expression>, so long as it is immediately surrounded by +parentheses. + +@s8<@i<Name Resolution Rules>> + +The expected type of a @fa<quantified_expression> is any Boolean type. +The @fa<predicate> in a @fa<quantified_expression> is expected to be of the same type. + +@s8<@i<Dynamic Semantics>> ---!corrigendum 4.5.9(0) +For the evaluation of a @fa<quantified_expression>, the @fa<loop_parameter_specification> +is first elaborated. The evaluation of a @fa<quantified_expression> then evaluates +the @fa<predicate> for each value of the loop parameter. These values are examined +in the order specified by the @fa<loop_parameter_specification> (see 5.5). +The value of the @fa<quantified_expression> is determined as follows: +@xbullet<If the @fa<quantifier> is @b<all>, the expression is True if the evaluation of the + @fa<predicate> yields True for each 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 False for a + 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 + @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: + +@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);> + + !ACATS test -Add an ACATS C-Test to test the syntax. +Add an ACATS C-Test to test the syntax and semantics. !appendix @@ -2527,6 +2623,26 @@ loop_parameter_specification). [Editor's Note: Version /05 fixes these errors.] + +**************************************************************** + +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: + +In !problem, I found 2 typos: + +the property A(I) <= A (I+1) obtains + ^^^^^^^ (holds) + +to indicate that all elemnts X satisfy + ^^^^^^^ (elements) + +In !proposal, I found 1 typo: + +that verify whether all (resp. al least one) + ^^ (at) ****************************************************************

Questions? Ask the ACAA Technical Agent