--- ai05s/ai05-0176-1.txt 2010/10/26 05:39:47 1.17 +++ ai05s/ai05-0176-1.txt 2010/11/19 05:36:23 1.18 @@ -1,5 +1,4 @@ -!standard 1.1.4(12) 10-10-15 AI05-0176-1/09 -!standard 2.9(2/2) +!standard 2.9(2/2) 10-11-18 AI05-0176-1/10 !standard 4.4(7) !standard 4.5.9(0) !reference AI05-0139-2 @@ -37,14 +36,12 @@ indicate the domain of definition of the element (which is some finite set). The common notation is: - for all X in domain | P (X) + for all X in domain => P (X) -[Editor's note: Change syntax to "=>"?? See e-mail of Sept. 15, 2010.] - Similarly, to indicate that at least one element of the domain satisfies a given property, we might write - for some X in domain | P (X) + for some 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 @@ -54,7 +51,7 @@ directly an element of the collection, and we can use the proposed syntax of AI05-0139-2 to write: - for all X of Directory | Name (X)'Length < 20 + for all X of Directory => Name (X)'Length < 20 Where Directory is some container, or an array. @@ -64,28 +61,22 @@ !proposal Introduce quantified expressions in the language, with their usual meaning: -boolean expressions that verify whether all (resp. at least one) element in a -collection (array or container) satisfies a given predicate. Introduce a -new reserved keyword: "some" to support this feature. +they are boolean expressions that verify whether all (resp. at least one) +element in a collection (array or container) satisfies a given predicate. +Introduce a new reserved keyword: "some" to support this feature. Quantified expressions have the following syntax: - ( for quantifier loop_parameter_specification | Boolean_Expression ) + ( for quantifier loop_parameter_specification => Boolean_Expression ) or - ( for quantifier iterator_specification | Boolean_Expression ) + ( for quantifier iterator_specification => Boolean_Expression ) The iterator_specification is the one proposed in AI05-0139-2 for -iterators. It includes default iterations over discrete ranges and over +iterators. It includes default iterations over discrete ranges, arrays, and containers, as well as user-defined iterations over such. !wording -Modify 1.1.4(12): - -* A vertical line separates alternative items unless it occurs immediately - 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: @@ -98,15 +89,11 @@ Syntax - quantified_expression ::= for quantifier loop_parameter_specification | predicate - | for quantifier iterator_specification | predicate + quantified_expression ::= for quantifier loop_parameter_specification => predicate + | for quantifier iterator_specification => predicate quantifier ::= all | some predicate ::= boolean_expression -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. @@ -125,9 +112,10 @@ 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 (see 5.5). +or iterator_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) or iterator_specification (see 5.5.1). The value of the quantified_expression is determined as follows: @@ -150,29 +138,27 @@ AARM ramification: The expression is False if the domain contains no values. *Some* is sometimes called "exists" in mathematical logic. -[Editor's note: This wording needs some description of how it works for an -iterator_specification -- but we can't do that until AI05-0139-2 gets closer -to completion.] - - Examples The postcondition for a sorting routine on an array A with an index subtype T can be written: -Post => (for all I in A'First .. T'Pred(A'Last) | A (I) <= A (T'Succ (I))) +Post => (A'Length < 2 + or else (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: - pragma Assert (for some X in 2 .. N / 2 | N mod X = 0); + pragma Assert (for some X in 2 .. N / 2 => N mod X = 0); !discussion -Instead of a vertical bar, we could use a colon or a right arrow to separate the -iterator from the condition. The proposed notation is more common in mathematics -but the vertical bar has already other uses in Ada syntax. +We have adopted the right arrow (=>) as a separator between the iterator +specification and the predicate. Other choices were suggested, but the arrow +is already used for this purpose in SPARK, and it seems preferable to be +consistent with this programming precedent, rather than with mathematical +convention, which uses a vertical bar. The order of evaluation is fixed by the iterator used in the loop_parameter_specification or iterator_specification, so there is a @@ -184,16 +170,7 @@ (See Wording.) -!corrigendum 1.1.4(12) -@drepl -@xbullet<A vertical line separates alternative items unless it occurs immediately -after an opening curly bracket, in which case it stands for itself:> -@dby -@xbullet<A vertical line separates alternative items unless it occurs immediately -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 @@ -216,8 +193,8 @@ @s8<@i<Syntax>> -@xcode<@fa<quantified_expression ::= >@ft<@b<for>>@fa< quantifier loop_parameter_specification | predicate - | >@ft<@b<for>>@fa< quantifier iterator_specification | predicate +@xcode<@fa<quantified_expression ::= >@ft<@b<for>>@fa< quantifier loop_parameter_specification => predicate + | >@ft<@b<for>>@fa< quantifier iterator_specification => predicate quantifier ::= >@ft<@b<all>>@fa< | >@ft<@b<some>>@fa< predicate ::= >@ft<@i<boolean_>>@fa<expression>> @@ -232,10 +209,11 @@ @s8<@i<Dynamic Semantics>> -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 +For the evaluation of a @fa<quantified_expression>, the @fa<loop_parameter_specification> or +@fa<iterator_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). +in the order specified by the @fa<loop_parameter_specification> (see 5.5) +or @fa<iterator_specification> (see 5.5.1). The value of the @fa<quantified_expression> is determined as follows: @@ -258,18 +236,28 @@ 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)))> +@xcode<Post =@> (@b A'Length < 2 + @b<or else> (@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 Add an ACATS C-Test to test the syntax and semantics. +!ASIS section + +New queries on quantified expressions: + + Iterator_Specification + Loop_Parameter_Specification + Predicate + Quantifier + !appendix From: Robert Dewar @@ -2681,11 +2669,11 @@ From: Randy Brukardt Sent: Friday, June 25, 2010 4:01 PM -> 4.5.7(4.a/3)... This is the same rule that is used for -> conditional_expressions; see 4.5.7 for a detailed discussion of the +> 4.5.7(4.a/3)... 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. -> -> Since this *is* 4.5.7, it seems strange to refer to this chapter in +> +> Since this *is* 4.5.7, it seems strange to refer to this chapter in > the sentence above. Actually, this cause is supposed to be numbered 4.5.9, and the above sentence refers @@ -2693,8 +2681,8 @@ draft. For that reason, I couldn't use the appropriate cross-reference, either, so I just left the reference and hopefully I'll remember to fix it in the future. -> I would propose that to (9/3) a remark is added that "Some" -> is what in mathematical logic is called "exists" and is the opposite +> I would propose that to (9/3) a remark is added that "Some" +> is what in mathematical logic is called "exists" and is the opposite > of "all". Probably a good idea. @@ -3368,13 +3356,13 @@ John wrote in his editorial review: -> This AI is very confused over whether the form with -> iterator_specification is included or not. It is in the !proposal. -> And in the !wording where the (loathsome) modification to the stuff -> about vertical line is described and in the syntax. But it is not in +> This AI is very confused over whether the form with +> iterator_specification is included or not. It is in the !proposal. +> And in the !wording where the (loathsome) modification to the stuff +> about vertical line is described and in the syntax. But it is not in > the dynamic semantics. -> But in the !corrigendum it is in the vertical line stuff but not in -> the syntax or dynamic semantics. So wording and corrigendum are +> But in the !corrigendum it is in the vertical line stuff but not in +> the syntax or dynamic semantics. So wording and corrigendum are > inconsistent. Given that "iterator_specification" is defined by an AI that is very much @@ -3384,14 +3372,14 @@ --- -> I must say for the umpteenth time that I hate this syntax using the -> vertical bar. The advantage of using "=>" instead seem to me to be so -> manifestly obvious that I still find it unbelievable that we are still +> I must say for the umpteenth time that I hate this syntax using the +> vertical bar. The advantage of using "=>" instead seem to me to be so +> manifestly obvious that I still find it unbelievable that we are still > using teh wretched bar. Well, I voted against both "|" and "=>", bar because this isn't an alterative or "or"; and "=>" because it looks too much like a case statement or aggregate -for my taste. +for my taste. Indeed, using "=>" would be very confusing with the aggregate syntax of

Questions? Ask the ACAA Technical Agent