--- 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 +but the vertical bar has already other uses in Ada syntax. + +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