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

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

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