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

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

--- ai05s/ai05-0176-1.txt	2010/02/04 07:11:43	1.4
+++ ai05s/ai05-0176-1.txt	2010/02/23 01:05:48	1.5
@@ -1,4 +1,4 @@
-﻿!standard 2.9(2/2)                                  10-02-03  AI05-0176-1/02
+﻿!standard 2.9(2/2)                                  10-02-22  AI05-0176-1/03
!standard 3.3(19)
!standard 4.4(7)
!standard 4.5.9(0)
@@ -12,65 +12,64 @@

!summary

-Syntax is proposed for universally quantified expressions over a finite domain.
+Syntax is proposed for quantified expressions over a finite domain.

!problem

It is very common in formal development to define a predicate over a collection
-to express the fact that all elements of the collection satisfy a given
-property, or that at least one element of the collection satisfies it. (This is
-of course 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). 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 programming
-language that is meant to be executable, and the syntax must indicate the domain
-of definition of the element. The common notation is:
-
-      forall X in domain | P (X),
-
-Similarly, to indicate that some element of the domain satisfies a given
-property, we write
-
-      exists 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 index (the
-bound variable in the expression) is used to denote an element of the collection
-in the condition. For collections with no built-in ordering, the bound variable
-denotes directly an element of the collection:
+to express the fact that all elements of the collection satisfy a given property
+or that at least one element of the collection satisfies it. (This is of course
+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).
+
+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
+programming language that is meant to be executable, and the syntax must
+indicate the domain of definition of the element (which is some finite set).
+The common notation is:
+
+    for all  X in domain | P (X),
+
+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)
+
+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
+index (the bound variable in the expression) is used to denote an element of the
+collection in the following predicate. When there is no defined index for the
+collection, and there is a default iterator for it, the bound variable denotes
+directly an element of the collection, and we can use the proposed syntax of
+AI05-0139-2 to write:

-         for all X in Directory | Name (X)'Length < 20
+      for all X of Directory | Name (X)'Length < 20

-Directory may be one of the predefined containers, or an array.
+Where Directory is some container, or an array.

-Such expressions will prove very useful in pre/post conditions and invariants.
+Quantified expressions will prove particularly useful in pre/postconditions
+and type invariants.

!proposal

Introduce quantified expressions in the language, with their usual meaning:
boolean expressions that verify whether all (resp. al least one) element in a
-collection (array or container) satisfies a given predicate. Introduce a new
-keyword: "exists" to support this feature.
+collection (array or container) satisfies a given predicate. Introduce a
+non-reserved keyword: "some" to support this feature.

Quantified expressions have the following syntax:

-   ( for all defining_identifier in Domain | Boolean_Expression )
+     ( for quantifier loop_parameter_specification | Boolean_Expression )

-   Domain =>  Discrete_Range | Expression
+The loop_parameter_specification is the one proposed in AI05-0139-2 for
+iterators. It includes default iterations over discrete ranges and over
+containers, as well as user-defined iterations over such.

!wording

-Add in 2.9 a new reversed word
-   exists
-
-Modify 3.3 (19):
-
-   * a loop parameter, choice parameter, quantified expression parameter,
-     or entry index;
-
Add to 4.4 (7) a new kind of primary:
quantified_expression

@@ -86,104 +85,60 @@

domain ::=  discrete_subtype_definition | expression
predicate ::= boolean_expression
-
-   Static Semantics
-
-A quantified expression declares a *quantified expression parameter*, whose
-subtype is defined by the domain:
-
-   * if the domain is a discrete_subtype_definition, this is the subtype of the
-     quantified expression parameter.

-   * if the domain is an expression that is a one-dimensional array, the subtype
-     of the quantified expression parameter is the element type of the array.
+Name Resolution Rules

-   * if the domain is an expression whose value is an instance of a container,
-     the subtype of the quantified expression parameter is the element type of
-     the container.
-
-   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.
+The predicate in a quantified_expression is expected to be of any boolean type.

-A predicate is expected to be of any boolean type.
+Dynamic Semantics

-   Dynamic Semantics
+The evaluation of a quantified expression 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
+  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.
+
+* 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.

-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
-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 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
-  the domain have been examined, or when the predicate yields True for a given
-  value.
+AARM note: the expression is False if the domain contains no values.

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

-[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)).]
+The postcondition for a sorting routine on arrays with can be written:

-!discussion
+Post => (for all I:T in A'First .. A (T'Pred(A'Last)) | A (I) <= A (T'Succ (I)))

-Instead of a vertical bar, we could use a colon to separate the iterator from
-the condition. The proposed notation is more common in mathematics.
+The assertion that a positive number is composite can be written:

-When quantifying over an array, the syntax provides the index, i.e. a cursor
-over the array. There is no obvious domain over which to define a cursor in the
-case of a container, so the notation  (for all X in C | P (X)) is natural.
-However, for the case of Maps, it would be attractive to have a form that binds
-both a key and the corresponding element in the container. This suggests
-introducing an attribute 'Domain  (we already have 'Range) so we could write
-
-     (for all Key in M'Domain ( Find (M, Key) > 7)
-
-Given that a mapping has a domain and a range, this suggests generalizing both
-of these attributes to be used in quantified expressions and in loops, but this
-is probably too big a change at this time.
+   (for some X in 2 .. N / 2 | N mod X /= 0)

!discussion
-
-Instead of a vertical bar, we could use a colon to separate the iterator from
-the condition. The proposed notation is more common in mathematics.

-When quantifying over an array, the syntax provides the index, i.e. a cursor
-over the array. There is no obvious domain over which to define a cursor in the
-case of a container, so the notation  (for all X in C | P (X)) is natural.
-However, for the case of Maps, it would be attractive to have a form that
-binds both a key and the corresponding element in the container. This suggests
-introducing an attribute 'Domain  (we already have 'Range) so we could write
-
-    (for all Key in M'Domain ( Find (M, Key) > 7)
-
-Given that a mapping has a domain and a range, this suggests generalizing both
-of these attributes to be used in quantified expressions and in loops, but
-this is probably too big a change at this time.
+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
+
+The order of evaluation is fixed by the iterator used in the
+loop_parameter_specification,  so there is a strong assumption of sequentiality.
+Not clear how to indicate that a quantified expression can be evaluated in
+parallel, given that we have no mechanism to parallelize loops either.

!example

-(See wording.)
+(See Wording.)

--!corrigendum 4.5.9(0)

@@ -1503,5 +1458,160 @@
"there_exists":

(for_all X in ...) and (there_exists X in ...)
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Thursday, February 4, 2010  3:08 AM
+
+> That's a huge bullet. When we discussed this back in November, I did a
+> quicky look at the code of a portion of Janus/Ada (about 25%) and
+> found more than 20 parameters and objects named "Exists". I just did a
+> look at the public part of Claw and found 4 overloaded functions named "Exists".
+
+Not as pretty as "exists", but wouldn't "is" work (if it does not introduce
+syntactic ambiguities):
+
+is X in D | P(x)
+
+****************************************************************
+
+From: John Barnes
+Sent: Thursday, February 4, 2010  3:41 AM
+
+I would prefer "for some" rather than "exists".  One problem with exists rather
+than there exists is that it seems a bit like a question rather than a
+statement.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Thursday, February 4, 2010  7:03 AM
+
+I like the symmetry for "for all" and "for some" .  An unreserved keyword is
+less of a disturbance than "exists".
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, February 4, 2010  7:12 AM
+
+I agree (significantly more implementation effort, but that's a minor issue in
+this case).
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, February 4, 2010  7:40 AM
+
+When I read maths texts, I pronounce the upside-down A as "for all" in my head,
+and the backwards E as "there exists".  Just "exists" by itself sounds odd to
+me.  I think "for some" reads nicely.
+
+I have no objection to unreserved keywords.
+
+****************************************************************
+
+From: Stephen Michell
+Sent: Thursday, February 4, 2010  8:15 AM
+
+How about a keyword thereexists, or there_exists. ?
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, February 4, 2010  8:30 AM
+
+> I think we have
+> to bite the bullet and introduce the keyword "exists".
+
+Unfortunately, there's a predefined function Exists in Ada.Directories!
+
+****************************************************************
+
+From: Steve Baird
+Sent: Thursday, February 4, 2010  11:18 AM
+
+> The evaluation of a quantified expression assigns to the
+> quantified_expression_parameter each one of the values specified by
+> the domain,
+
+I think we need to make clear that no assignment is taking place, at least in
+the case of a by-reference type. This is more like the actual-to-formal binding
+of a subprogram call - no adjust/finalize calls, no issues with limited types.
+
+Incidentally, I think the proposed wording correctly handles the case where the
+domain is empty (result is True for "for-all", False for "for-some"), but I
+wonder if AARM clarification of this point would be a good idea.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Thursday, February 4, 2010  12:11 PM
+
+> I think we need to make clear that no assignment is taking place, at
+> least in the case of a by-reference type.
+> This is more like the actual-to-formal binding of a subprogram call -
+> no adjust/finalize calls, no issues with limited types.
+
+Good point. Can we say that the parameter is bound to each value in the domain?
+in usual parlance, that thing is called the bound variable,  but i did not want
+to use "variable" if this is to be treated like a loop_parameter.
+
+> Incidentally, I think the proposed wording correctly handles the case
+> where the domain is empty (result is True for "for-all", False for
+> "for-some"), but I wonder if AARM clarification of this point would be
+> a good idea.
+
+Sure.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, February 22, 2010  4:43 PM
+
+[Attached was version /03 of the AI. - Editor]
+This is now much simplified because based on AI05-0149 (iterators).
+The semantics is sequential because that's what we say about iterators as well.
+Instead of the unpalatable "exists" we now have a non- reserved keyword "some" .
+The rest seems straightforward.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, February 22, 2010  6:55 PM
+
+> This is  now much simplified because based on AI05-0149
+> (iterators).
+
+I presume you mean AI05-0139-2 here, AI05-0149 is "access subtype conversion and
+membership". I changed the AI writeup this way.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, February 22, 2010  5:28 PM
+
+The last line of the "Examples" section
+doesn't fly, in my book:
+
+   The assertion that a positive number is
+   composite can be written:
+
+    (for some X in 1 .. N / 2 | N mod X /= 0)
+
+-----
+
+I would have expected:
+
+    (for some X in 2..N/2 | N mod X = 0)
+
+implies N is composite, while:
+
+    (for all X in 2..N/2 | N mod X /= 0)
+
+implies N is prime.
+
+Or am I confused?

****************************************************************

Questions? Ask the ACAA Technical Agent