!standard 2.9(2/2) 10-11-18 AI05-0176-1/10 !standard 4.4(7) !standard 4.5.8(0) !reference AI05-0139-2 !class Amendment 09-10-28 !status Amendment 2012 10-06-03 !status ARG Approved 8-0-0 11-02-18 !status work item 10-10-15 !status ARG Approved 7-0-3 10-06-18 !status work item 10-06-18 [rejected by WG 9] !status ARG Approved 6-1-3 10-02-27 !status work item 09-10-28 !status received 09-10-28 !status received !priority Low !difficulty Easy !subject Quantified expressions !summary Syntax is added 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) 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 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 of Directory => Name (X)'Length < 20 Where Directory is some container, or an array. Quantified expressions will prove particularly useful in pre/postconditions and type invariants. !proposal Introduce quantified expressions in the language, with their usual meaning: 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 ) or ( 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, arrays, and containers, as well as user-defined iterations over such. !wording Add "some" to the list of reserved words in 2.9(2/2). Add to 4.4 (7) a new kind of primary: quantified_expression Add a new clause (after the proposed clauses for conditional expressions (AI05-0147) and case expressions (AI05-0188-1): 4.5.8 Quantified expressions Syntax quantified_expression ::= for quantifier loop_parameter_specification => predicate | for quantifier iterator_specification => predicate quantifier ::= all | some predicate ::= boolean_expression 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 of the same type. Dynamic Semantics For the evaluation of a quantified_expression, the loop_parameter_specification 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: * 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 ramification: The expression is True if the domain contains no values. * 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 ramification: The expression is False if the domain contains no values. *Some* is sometimes called "exists" in mathematical logic. Examples The postcondition for a sorting routine on an array A with an index subtype T can be written: 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); !discussion 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 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.) !corrigendum 2.9(2/2) @dinsl @b !corrigendum 4.4(7) @drepl @xcode<@fa @fa@ft<@b>@fa< | string_literal | aggregate> @fa<| name | qualified_expression | allocator | (expression)>> @dby @xcode<@fa @fa@ft<@b>@fa< | string_literal | aggregate> @fa<| name | qualified_expression | allocator | (expression) | (quantified_expression)>> !corrigendum 4.5.8(0) @dinsc @s8<@i> @xcode<@fa@ft<@b>@fa< quantifier loop_parameter_specification =@> predicate | >@ft<@b>@fa< quantifier iterator_specification =@> predicate quantifier ::= >@ft<@b>@fa< | >@ft<@b>@fa< predicate ::= >@ft<@i>@fa> Wherever the Syntax Rules allow an @fa, a @fa may be used in place of the @fa, so long as it is immediately surrounded by parentheses. @s8<@i> The expected type of a @fa is any Boolean type. The @fa in a @fa is expected to be of the same type. @s8<@i> For the evaluation of a @fa, the @fa or @fa is first elaborated. The evaluation of a @fa then evaluates the @fa for each value of the loop parameter. These values are examined in the order specified by the @fa (see 5.5) or @fa (see 5.5.1). The value of the @fa is determined as follows: @xbullet is @b, the expression is True if the evaluation of the @fa yields True for each value of the loop parameter. It is False otherwise. Evaluation of the @fa stops when all values of the domain have been examined, or when the @fa yields False for a given value. Any exception raised by evaluation of the @fa is propagated.> @xbullet is @b, the expression is True if the evaluation of the @fa yields True for some value of the loop parameter. It is False otherwise. Evaluation of the @fa stops when all values of the domain have been examined, or when the @fa yields True for a given value. Any exception raised by evaluation of the @fa is propagated.> @s8<@i> The postcondition for a sorting routine on an array A with an index subtype T can be written: @xcode (A'Length < 2 @b (@b I @b 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 Assert (@b X @b 2 .. N / 2 =@> N @b 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 Sent: Thursday, March 5, 2009 2:44 PM ... And while we are at it, if we are talking useful stuff in PPC's, how about adding quantifiers while we are at it (for all X in Sint => Sqrt (X) < 23) or something like that ... **************************************************************** From: Ed Schonberg Sent: Thursday, March 5, 2009 2:52 PM Would mesh nicely with some new iterator forms, of course... There is no concern here that the iteration might not finish. **************************************************************** From: Ed Schonberg Sent: Sunday, March 15, 2009 9:07 AM > where lhs is the same (possibly complex) lhs. much cleaner and clearer > to write > > lhs := (if bla then 3 else 4); Agreed, this will be used abundantly. I like the default boolean True interpretation when the else part is missing. Not convinced about the need for case expressions, but would like to see a similar proposal for what Randy calls loop expressions, i.e. quantified expressions. **************************************************************** From: Robert Dewar Sent: Sunday, March 15, 2009 9:30 AM The tricky issue in quantifiers is how to deal with iterators. **************************************************************** From: Ed Schonberg Sent: Sunday, March 15, 2009 9:41 AM Of course, but the point is to find a very light syntax, so this is not necessarily tied up to the full iterator proposal that Randy developed. To be useful is should cover both arrays and containers with a similar syntax, and should mention elements, not cursors, something like (for all E in A : F (E) > 0) If this is defined as a tampering context we can probably simplify semantics and termination issues. Should this be short-circuited? etc. **************************************************************** From: Robert Dewar Sent: Sunday, March 15, 2009 10:20 AM Definitely short circuited, this is a search for a counterexample and no point in continuing once a counterexample has been found. The question to me is does this only work with built in containers, or is there a way to make your own containers pick up the iteraction. Also do we have (exists E in A : F(E) > 0) con: another keyword pro: a bit more transparent then not (for all E in A : F(E) <= 0) Also, are we sure : is right, I think | might be better (for all E in A | F (E) > 0) though I guess to some mathematicians it will read as such that, and perhaps we should allow the full notation (for all E in A | E > 0 : F (E) > 0) read "for all E in A such that E > 0, it is the case that F (E) > 0" BTW, an implementation is allowed and perhaps encouraged to allow the forall symbol to replace for all as a representation alternative. Could even require it (surely a better use of invading mysterious characters in the language proper than pi in the numerics stuff!) **************************************************************** From: Bob Duff Sent: Sunday, March 15, 2009 9:46 AM ... >...but would like to > see a similar proposal for what Randy calls loop expressions, i.e. > quantified expressions. I've no idea what quantified expressions should look like or mean, so I too would like to see a proposal. Didn't Cyrille volunteer to send one to ada-comment? **************************************************************** From: Edmond Schonberg Sent: Monday, March 16, 2009 2:08 PM > I've no idea what quantified expressions should look like or mean, so > I too would like to see a proposal. Didn't Cyrille volunteer to send > one to ada-comment? I'm sure you do, you just forgot! Quantified expressions are first- order formulae over sets (that is to say any kind of container). They are either universal (using the forall quantifier) or existential (using the exists quantifier). They use a bound variable to indicate some property of elements of the set. So for example : forall X in S | P (X) which is True is all elements of S satisfy property P. The existential quantifier is redundant, because we can always rewrite: Exists X in S | P (X) as not (forall X in S | not P (X)) but it' cheap and nicer to have both quantifiers. The run-time semantics of such a construct are short-circuited, i.e. the implicit iteration stops as soon as an example has been found. The necessary constituents are a container and a predicate. The scope of the bound variable is the body of the predicate. Now figure out the best syntax for this, preferably one that feels natural in Ada! **************************************************************** From: Randy Brukardt Sent: Monday, March 16, 2009 2:17 PM > I'm sure you do, you just forgot! Quantified expressions are > first- order formulae over sets (that is to say any kind of > container). They are either universal (using the forall > quantifier) or existential (using the exists quantifier). > They use a bound variable to indicate some property of elements of the > set. Could you translate this into English? This sounds like some philosophy class run amok. :-) (Specifically, what do you mean by "universal" and "existential" here??) **************************************************************** From: Edmond Schonberg Sent: Monday, March 16, 2009 2:36 PM Now now, just look at the examples. A universally quantified expression says: all elements of this set have this particular property. An existentially quantified one says : there does exist one element of this set that satisfies this property . Both of these are in fact loops over a set, and their naive implementation is: forall := false; Elmt := First_Element (S); while Present (Elmt) loop if not P(X) then forall := False; exit; end if; Next_Elmt (Elmt); end loop; And the converse for Exists. This conventional interpretation means that a universally quantified expression over a null set is always true (all the elements of the empty set are green, for example). The rest is syntax. Conventional mathematical notation is Forall (X) (P (X)) which is tricky to implement because it doesn't say where X comes from (the domain is implicit in the condition itself). For an executable programming language you want to specify the domain explicitly, and unless you have lazy evaluation you want the domain to be finite. A number of years ago SETL chose the notation (forall X in S | P(X)). Instead of the vertical bar I've seen suggestions for a colon, maybe closer to existing conventions in C- languages. **************************************************************** From: Randy Brukardt Sent: Monday, March 16, 2009 3:01 PM Thanks for the clear explanation. This one I understand (and probably use from time-to-time, I just didn't know it had a name). **************************************************************** From: Robert Dewar Sent: Monday, March 16, 2009 2:39 PM > Could you translate this into English? This sounds like some > philosophy class run amok. :-) No, more like a review of a very elementary math course :-) > (Specifically, what do you mean by "universal" and "existential" > here??) Well here I can't follow Randy's I-dont-know-no-stinking-math philosophy universal and existential quantifiers seem totally familiar and natural to me. **************************************************************** From: Randy Brukardt Sent: Monday, March 16, 2009 2:59 PM > No, more like a review of a very elementary math course :-) Sorry, Robert, the last formal math course I took was 29 years ago. Unless I've had reason to use the information in my day-to-day work, I've almost certainly forgotten it. > > (Specifically, what do you mean by "universal" and "existential" > > here??) > > Well here I can't follow Randy's I-dont-know-no-stinking-math > philosophy universal and existential quantifiers seem totally familiar > and natural to me. I think it is the terms "universal quantifiers" and "existential quantifiers" here that threw me; Ed explains an "if all" and "if exist" (that's the backwards E if I remember right) relationship. That I understand; I still don't remember ever hearing them given these names. Sorry if that offends your sense of math correctness (a version of political correctness, I think). **************************************************************** From: Robert Dewar Sent: Monday, March 16, 2009 4:33 PM > I think it is the terms "universal quantifiers" and "existential > quantifiers" here that threw me; Ed explains an "if all" and "if exist" > (that's the backwards E if I remember right) relationship. That I > understand; I still don't remember ever hearing them given these names. See you *do* remember stuff from all that time ago :-) > Sorry if that offends your sense of math correctness (a version of > political correctness, I think). Something like that no doubt, it's part of the secret handshake of mathematicians :-) **************************************************************** From: Tucker Taft Sent: Monday, March 16, 2009 3:14 PM Randy, I think you should probably drag out one of those old math textbooks if we are going to be talking about preconditions and postconditions. Existential (there exists) and universal (for all) quantifiers are pretty fundamental (as is "implies" by the way ;-). I think it is healthy for us to reexamine whether these standard logic notions are appropriate for a programming language (at least you convinced me that "implies" doesn't quite work for our purposes), but we should at least be able to use the vocabulary of first-order logic in our *discussions*. There are a lot of good books out there, and of course there is Wikipedia, which probably has all you need. A good starting point might be: http://en.wikipedia.org/wiki/First-order_logic One book I have used is: Software Engineering Mathematics by Jim Woodcock and Martin Loomes SEI series in Software Engineering, 1988. This one is clearly aimed at programmers who want to get more "formal" in their approach to software engineering. It also happens to use "Zed" notation (simply "Z" in the UK), which is pretty popular among the formal methods crowd. **************************************************************** From: Randy Brukardt Sent: Monday, March 16, 2009 3:44 PM > Randy, I think you should probably drag out one of those old math > textbooks if we are going to be talking about preconditions and > postconditions. > Existential (there exists) and universal (for all) quantifiers are > pretty fundamental (as is "implies" by the way ;-). I agree that they are fundamental, I just had never heard these names before. ... > I think it is healthy for us to > reexamine whether these standard logic notions are appropriate for a > programming language (at least you convinced me that "implies" doesn't > quite work for our purposes), but we should at least be able to use > the vocabulary of first-order logic in our *discussions*. Not with me, sorry. I didn't take the logic class at UW, taking statistics and probability instead. (I think the former may have been taken while I was still a ChemE, so I had the credits when I transferred to a CS major.) > There are a lot of good books out there, and of course there is > Wikipedia, which probably has all you need. A good starting point > might be: > > http://en.wikipedia.org/wiki/First-order_logic OK, thanks for the reference. A quick look at this shows its going to take a lot longer than a few minutes to make sense out of this. It'll have to wait a few weeks at least, until ASIS and the minutes and the conference call are done. [BTW, I think "first-order logic" is "and", "or", and "not". Anything more complicated than that clearly has a higher order. ;-)] **************************************************************** From: Edmond Schonberg Sent: Monday, March 16, 2009 3:33 PM > I think it is healthy for us to > reexamine whether these standard logic notions are appropriate for a > programming language (at least you convinced me that "implies" doesn't > quite work for our purposes), but we should at least be able to use > the vocabulary of first-order logic in our *discussions*. I think the semantics of quantified expressions are intuitive and straightforward to implement. They are particularly useful in pre- and postconditions but have more general uses. The transformation of a quantified expression into a loop is immediate, and also leads naturally to nested loops when a condition is defined over elements of two sets: (forall X in S1, Y in S2 : P (X, Y)) One nice thing about these implicit iterators is that they do not mention cursors but speak directly about elements. I suppose that the expression can be defined to be a tampering context, so that any perverse use of the condition to modify an element will be rejected. The more general question is whether this is too much machinery to add to the language at this point. **************************************************************** From: Tucker Taft Sent: Monday, March 16, 2009 3:57 PM The obvious alternative is to rely on programmers writing appropriate named functions that do the iteration internally. I don't think forcing the definition of named functions is appropriate for conditional expressions, but for quantified expressions, I think expecting the programmer to program up an appropriate named function is not too much to ask. So I see these quantified expressions as significantly lower priority than conditional expressions. **************************************************************** From: Robert Dewar Sent: Monday, March 16, 2009 4:38 PM Note that in Setl you routinely write an expression which is pronounced for all x in some-set such that p(x) is true, it is the case that q (x) is also true. that "such that" phrase is certainly convenient to have in practice, and the mathematical crowd will be quick to point this out as a use of implies forall X in some-set | p(x) -> q(x) and in that context the -> reads pretty nicely I think but most likely forall X in someset | (if p(x) then q(x)) the reason I like the such that phrase is that it is not so much that you want to consider that somehow p(x) implies q(x), it is more like you only want to consider the subset for which p(x) is true. This is logically equivalent, but feels different, so a notation like forall X in someset | p(x) : q(x) reads clearer to me (though I think I would prefer to use the vertical bar for the "it is the case that", rather than colon. **************************************************************** From: Robert Dewar Sent: Monday, March 16, 2009 4:41 PM > The obvious alternative is to rely on programmers writing appropriate > named functions that do the iteration internally. I don't think > forcing the definition of named functions is appropriate for > conditional expressions, but for quantified expressions, I think > expecting the programmer to program up an appropriate named function > is not too much to ask. > > So I see these quantified expressions as significantly lower priority > than conditional expressions. Well there is the issue of bodies in the spec, and it does not seem that you can use renaming of expressions to achieve this if you don't have quantified expressions. I find the bodies-in-spec issue to be a significant one! **************************************************************** From: Bob Duff Sent: Monday, March 16, 2009 5:15 PM > I'm sure eou do, you just forgot! ... Thanks for the mathematical logic lesson, but I think you misunderstood what I meant. ;-) I understand what universal quantifiers are in maths, and I haven't forgotten my logic course (at least, I haven't forgotten therbasics). I even taught this stuff to Bill some time ago, and he understands, for example, why "all pink unicorns are green" is true. What I meant is that I don't know how this stuff should be translated into a programming language, especially an imeerative programming language like, say, Ada. Given your recent comments, you are thinking that "for all" is just syntactic sugar for a loop. No big deal But it sounded like Cyrille was thinking of something more "math-y". Maths doesn't have loops. Nor side effects. Nor "run time" vs. "compile time". In maths we are comfortable talking about infinite sets, and combinatorially huge sets. A type (in Ada) has (or is?) a set of values. I was wondering if one can say things like "for all values X, Y, and Z of type String, X >= Y and Y >= Z implies X >= Z". This means all _possible_ values, not just all values that some program happens to have computed so far. And a mathemetician would point out that Natural'Last can be arbitrarily large, and would like to prove the above for all possible implementations of Ada. But that's apparently not what you mean by universal quantifiers in Ada. **************************************************************** From: Robert Dewar Sent: Monday, March 16, 2009 7:10 PM Clearly the sets in this case have to be finite, and the notion of quantifiers over finite sets is well established in mathematics. So, no you cannot have non-effective quantifiers over infinite sets, you could expect to say; (for all A in Integer | P (A)); but it would take a long time to compute this :-) **************************************************************** From: Robert I. Eachus Sent: Monday, March 16, 2009 8:39 PM Let me try to bring this discussion out of the blue sky and back to the practical. The primary goal of any extensions to Ada should be:to make programs easier to write. As long as doing so does not make the programs more difficult to read and understand, and as long as the extensions do not make it easier to write bad (in some existential sense) programs than good programs. There are going to be many other criteria about making the language easier or harder to learn, to implement, or to prove correct. Plus to some extent a concern about creating too big a language or a language that is not Ada. So what would we expect to gain or lose from adding for all to Ada? We currently have for subtypes: for I in Subtype'Range loop...end loop; The same syntax works for arrays: for I in A'Range loop..end loop; But for lists and other containers? Define what should be the body of the loop as a procedure with a parameter of type Cursor, inside the body of the procedure use calls to Element, and replace Element, or create more procedure declarations, and finally call Iterate passing the container and the procedure. In my humble opinion, the worst part of all that is not needing to know about throwaway things like Cursors, but having to write often simple code out of line. declare procedure Nonsense_Name(C: in Cursor) is begin if Element(C).Last_Modified = Today then Update_Element(Container, C, Daily_Backup; end if; end Nonsense_Name; begin Iterate(Container; Nonsense_Name; end; -- if Daily_Backup has other parameters, I need another wrapper procedure. Not very lightweight, especially if you use declare blocks to keep the wrapper procedure close by. If you could pass a declare block in-line it would make iterators much more comfortable to use and easier on readers as well. (Implementation shouldn't be that hard, this is really syntactic sugar, with access subprogram parameters already in the language.) Renaming Iterate: ;=) For_All(Element, Container, (if Element.Last_Modified = Today then Daily_Backup(Element); end if)); -- assumes that a declare block passed as a parameter would be wrapped -- in parentheses, not declare..end Is it worth stopping there, or is it worth going further? When Ada was first being defined, I suggested defining a couple of "extra" operator names with no associated operations. These could be used to name operations which didn't match the standard set of operations. I don' t know if that ever got as far as being thrown out in scope reductions in the 1983 or 1995 standards. But here what we would really like is a template which takes two arguments and a block of code: for all Element in Container do begin if Element.Last_Modified = Today then Daily_Backup(Element); end if; end; There could be generic templates like this declared in Standard that could be instantiated for (pairs of) types to create both for all and exists type functionality. However, I think I am reaching well beyond what should be considered for the next version of Ada. Besides, the huge improvement comes from putting the sequence of statements in line, the syntactic sugar is pretty, but doesn't add much. The anonymous declare block parameters may be a winner, especially if it can be merged with Randy's function renaming idea, by doing the same with renaming expressions as functions: function renames end [identifier]; Hmm. I think I see a problem, the first things I want to write are things like Factorial or Ackermann's function: function Factorial(N: Positive) return Integer renames (if N = 0 then 1 else N * Factorial (N-1)); end Factorial; function Ackermann(M, N: Positive) return Integer renames (if M = 0 then N+ 1 elsif N = 0 then Ackermann(M-1, N) else N * Ackermann (M-1, Ackermann(M,N-1))) end Ackermann; Should the recursive calls be disallowed (probably by making the name not visible)? Or do we just accept that theorem provers can run into lots of cases where the proof is possible, but takes a lot of CPU cycles? Certainly these functions are well defined, even if it does make more sense to use a BigNum type for the results. (For that matter it might be nice to add an Unbounded_Integer type in the Numerics annex.) Note that this example code for Ackermann, is really just syntactic sugar. Well... I save three return keywords, and some semicolons in exchange for some parentheses. I don't have a begin, but I do have a renames. The huge mental savings come from combining the spec and body, and putting the body (hopefully) where it is needed. Looking back, my practical may look pretty blue sky to some of you, but don't lose my point. Providing access to subprogram parameters makes a lot of things more doabile in Ada, but in practice the "out lining" of the code becomes pretty heavy. I try to use declare blocks to bring code back to almost where it should be, but it is still pretty heavy for what should be simple operations. Randy's renaming of expressions as functions has the same intended purpose, but in the case of package specifications, declare blocks don't help. **************************************************************** From: Randy Brukardt Sent: Monday, March 16, 2009 9:03 PM Proper iterators for Ada are discussed in AI05-0139-1, and were discussed at the Tallahassee meeting. Proper accessors for Ada are discussed in AI05-0142-1, on several recent threads on Ada-Comment (esp. the one about light-weight subprogram definitions for anonymous access types), and will be on the agenda of the upcoming subcommittee meeting. We're obviously interested in improving Ada in these areas. But it's not particularly helpful to rehash all of the points that have already been covered in these AIs and their e-mail threads. **************************************************************** From: Edmond Schonberg Sent: Monday, March 16, 2009 9:26 PM [Editor's note: Forked back from AC-0180.] > I agree. Large Boolean expressions are notoriously hard to read and > debug. I think we all agree on that. But to come back to the topic, quantified expressions by themselves are compact and easy to read, and therefore are a good choice to have in preconditions. Sortedness? (for all I in A'first .. A'last -1 : A(I) <= A (I+1)) If the preconditions have a very complex description that requires them being off-line, this may be a design issue, not a problem with boolean expressions per se! **************************************************************** From: Tucker Taft Sent: Monday, March 16, 2009 10:54 PM I think if we talk about object-oriented abstractions, then the "class-wide" / "inheritable" preconditions are almost certainly going to be described using (abstract) primitive functions, which are inevitably something you can't put in the spec. E.g. for an abstract Stack, the precondition on "Pop(Stack)" is "not Is_Empty(Stack)" and it is clear that Is_Empty will have to be defined differently for each concrete extension of the abstract Stack type. If we are talking about scalar or array-of-scalar abstractions I can see these things being fully defined in the spec, but for an abstraction which is truly "abstract" (either in the O-O sense or in the private-type sense), then the predicates are themselves going to involve abstract/private functions. These abstract predicates are in some sense "defined" by where they appear in preconditions and postconditions. E.g., if the postcondition of "Push(Stack) is "not Is_Empty(Stack)", and the precondition of "Pop(Stack)" is the same, then we know that a Pop immediately following a Push is safe. If we went further and defined a "Depth(Stack)" then we could get more specific, such as having a postcondition for Push of "Depth(Stack) = Depth(Stack)'old + 1" and a precondition on Pop of "Depth(Stack) > 0", and a postcondition of "Depth(Stack) = Depth(Stack)'old - 1". Combined with a postcondition on Depth(Stack) itself of "Depth'Result >= 0" then we can begin to understand the stack-like nature of a Stack, without ever seeing the body for "Depth". I believe that most "interesting" abstractions will have this characteristic, that is, where it will be necessary to define "helper" functions to specify pre- and postconditions, and the meaning of the helper functions will be implicit in how they are used in pre- and postconditions (I'll admit that sounds circular), and not require visibility on the body of these helper functions, some of which may be "abstract" when talking about O-O type hierarchies. Given this, I am dubious about investing heavily in quantified expression syntax. Even for things like "sorted" I think you can't expect many compilers to glean the truth of your "for all" expression from the code, but if you claim via a postcondition of your sort routine that "Sorted(QSort'Result)" and elsewhere you have a precondition of "Sorted(A)", then it would not be too much of a leap for the compiler to expect you to have defined "A" by using QSort or some other sorting routine, before calling a function that expected "Sorted(A)" to be True. To put this another way, I believe that from the *caller* side, pre- and postconditions will be treated more "symbolically," where it is the matching up of postconditions and preconditions which will be used to be sure that an object is in the right "state" before being passed to some operation. On the *callee* side, I believe the pre- and postconditions will actually be analyzed in their full glory, because that is the place where they are guaranteed to actually mean something, since that is where you have full access to the representation, and in an O-O context, you actually know the concrete type of the thing you are manipulating. **************************************************************** From: Bob Duff Sent: Monday, November 16, 2009 10:54 PM AI05-0176-1, Quantified expressions was mentioned recently. I think we should have an e-mail discussion of this issue, which was raised by John Barnes at the recent meeting: If we're going to have the universal quantifier "for all", we ought to also have the existential quantifier. John suggested the syntax "for some", which I like. It looks pretty silly to have one without the other -- reading the double negative (not (for all... (not...))) is pretty ugly. Sort of like having "and then" but not "or else" in the language. Are we willing to tolerate the new reserved word "some"? I'm not sure where I stand, but I'm in kind of a "both or neither" mood right now. **************************************************************** From: Robert Dewar Sent: Monday, November 16, 2009 5:11 PM The other possibility is of course exists. How about we do a run on the GNAT test suite to see how much use of either identifier there is. I will post results on this ASAP. **************************************************************** From: Bob Duff Sent: Monday, November 16, 2009 5:36 PM Good idea. FWIW, "for some" reads nicely to me. I'm not sure whether you're suggesting "for exists" or "if exists". To me, "for exists" looks weird. But I don't like "if exists" either, because it's a loop, so should have "for". I shall refrain from suggesting a backwards E, which I guess exists (heh heh) somewhere in Unicode. ;-) **************************************************************** From: Robert Dewar Sent: Monday, November 16, 2009 5:46 PM to me it is fine to write if for all ... if exists really the first line should be if forall ... and really we should allow the special symbols (gosh, we have them available in the 32-bit character set I am sure :-) :-) :-) while for some ... seems less nice to me than while exists but then I am biased by having programmed using while exists and while forall for many decades. > I shall refrain from suggesting a backwards E, which I guess exists > (heh heh) somewhere in Unicode. ;-) Well as per above, you are only allowed to suggest this if you suggest the corresponding symbol for FORALL :-) **************************************************************** From: Edmond Schonberg Sent: Monday, November 16, 2009 5:49 PM "exists" stands by itself to define a quantified expression: if exists X in S: .... or while exists X in S: .... I find it slightly preferable to "for some" **************************************************************** From: Gary Dismukes Sent: Monday, November 16, 2009 5:49 PM > FWIW, "for some" reads nicely to me. I'm not sure whether you're > suggesting "for exists" or "if exists". To me, "for exists" looks > weird. But I don't like "if exists" either, because it's a loop, so should > have "for". I suspect that 'some' is very rare, whereas I can easily imagine there are programs using 'exists' (as a predicate function name). > I shall refrain from suggesting a backwards E, which I guess exists > (heh heh) somewhere in Unicode. ;-) ;-) **************************************************************** From: Tucker Taft Sent: Monday, November 16, 2009 7:09 PM Actually, we do have the mathematical symbols to draw on. Pi got its nose in the tent for Ada 2005, Perhaps we could adopt ? and ? directly. **************************************************************** From: Bob Duff Sent: Monday, November 16, 2009 7:12 PM Edmond Schonberg wrote: > "exists" stands by itself to define a quantified expression: if > exists X in S: .... or while exists X in S: .... > > I find it slightly preferable to "for some" Ed, your comment, and Robert's similar comment, seem somewhat convincing to me, but I think I need to see the full BNF syntax before I can really "see" it. Gary's comment: > I suspect that 'some' is very rare, whereas I can easily imagine there > are programs using 'exists' (as a predicate function name). is a strong argument for 'some', but let's see the result of Robert's experiment first. > > I shall refrain from suggesting a backwards E, which I guess exists > > (heh heh) somewhere in Unicode. ;-) > > Well as per above, you are only allowed to suggest this if you suggest > the corresponding symbol for FORALL :-) Yes, of course. ;-) I shall also refrain from suggesting an upside-down A. I couldn't type an upside-down A on my keyboard to save my life! My opinion: You shouldn't have to know any more than 4'th grade math to learn how to program. **************************************************************** From: Tucker Taft Sent: Monday, November 16, 2009 8:59 PM > Actually, we do have the mathematical symbols to draw on. Pi got its > nose in the tent for Ada 2005, That was a mistake, IMHO. > Perhaps we could adopt ? and ? directly. Cool! Those look like upside-down A and backwards E on my screen! I've no idea how you typed them in. I hope you're kidding, Tuck. We really don't want the predefined stuff to depend on anything but 7-bit ASCII. It's fine to allow another 2**N characters, for N=31 or whatever, but let's not put that in the predefined stuff. P.S. Actually, that upside-down A has an extra serif on the side that looks weird to me. And probably looks weird to Donald Knuth. **************************************************************** From: Randy Brukardt Sent: Monday, November 16, 2009 9:16 PM > > Actually, we do have the mathematical symbols to draw on. Pi got its > > nose in the tent for Ada 2005, > > That was a mistake, IMHO. That's just an identifier, and there is an ASCII equivalent. Any user could have done the same. > > Perhaps we could adopt ? and ? directly. > > Cool! Those look like upside-down A and backwards E on my screen! > I've no idea how you typed them in. On my screen, I just see ? and ?. Not very helpful. (I'd type them in opening the symbol page in OpenOffice or Word, inserting them into a blank document, and then cut-and-pasting them into my e-mail. Not fun. Probably a programming editor would have a similar page, so it wouldn't be quite that bad in practice.) In any case, I have to remove characters like that from the filed mail, or I get complaints about "garbage" in the files. So please minimize the use of them here. > I hope you're kidding, Tuck. We really don't want the predefined > stuff to depend on anything but 7-bit ASCII. It's fine to allow > another 2**N characters, for N=31 or whatever, but let's not put that > in the predefined stuff. I wouldn't object if they were identifiers and there were regular ASCII representations available as well. (As in the PI case.) But to use them *in place* of reserved words is really nasty. So I too hope Tucker was kidding. **************************************************************** From: Tucker Taft Sent: Monday, November 16, 2009 9:44 PM >> Perhaps we could adopt ? and ? directly. > > Cool! Those look like upside-down A and backwards E on my screen! > I've no idea how you typed them in. The joys of using a Mac (and UTF-8). ;-) ... > P.S. Actually, that upside-down A has an extra serif on the side that > looks weird to me. And probably looks weird to Donald Knuth. The pain of infinite font choices. ;-( **************************************************************** From: Randy Brukardt Sent: Monday, November 16, 2009 11:52 PM > > Cool! Those look like upside-down A and backwards E on my screen! > > I've no idea how you typed them in. > > The joys of using a Mac (and UTF-8). ;-) For what it's worth (probably $0.00 :-), neither of those characters appear in the "special symbols" page of OpenOffice for the fonts provided with Windows XP. I believe OpenOffice shows all of the characters defined in the fonts (it is around a thousand characters for Times New Roman, including a lengthy set of Arabic characters -- but only a handful of math characters); it is nice enough to show the (Unicode) encoding of the characters. I suppose its possible that I looked in the wrong place; what codes are those characters?? **************************************************************** From: Randy Brukardt Sent: Monday, November 16, 2009 11:59 PM Following up, I found these in the Symbol font, with character codes F022 and F024; those codes are in the "private use area" and doesn't have the same glyphs in other fonts. So I'm pretty sure that typical Windows fonts don't have those characters. Which suggests against using them (having to use a special font to display them is obnoxious at best). (Haven't checked Windows 7 yet, perhaps it has more characters.) **************************************************************** From: Jean-Pierre Rosen Sent: Tuesday, November 17, 2009 4:09 AM > "exists" stands by itself to define a quantified expression: if > exists X in S: .... or while exists X in S: .... > > I find it slightly preferable to "for some" > So do I - but of course I am part of the gang under SETL influence ;-) **************************************************************** From: Robert Dewar Sent: Tuesday, November 17, 2009 6:34 AM > Actually, we do have the mathematical symbols to draw on. Pi got its > nose in the tent for Ada 2005, Perhaps we could adopt ? and ? > directly. Tee hee, someone rose to the bait! The introduction of Pi in the library was a HUGE pain, it required all sorts of special fiddling for us to deal with. I really don't want to get into this for the language itself. We could possibly allow these as alternatives, but you don't want to insist on them. In many environments this would simply make the features unavailable. **************************************************************** From: Robert Dewar Sent: Tuesday, November 17, 2009 6:36 AM >> I suspect that 'some' is very rare, whereas I can easily imagine >> there are programs using 'exists' (as a predicate function name). > > is a strong argument for 'some', but let's see the result of Robert's > experiment first. I don't think "I suspect" can ever be a "strong argument". Indeed let's wait for the result of the experiment. **************************************************************** From: Robert Dewar Sent: Tuesday, November 17, 2009 6:37 AM > Cool! Those look like upside-down A and backwards E on my screen! > I've no idea how you typed them in. not on my screen :-) **************************************************************** From: Robert Dewar Sent: Tuesday, November 17, 2009 6:38 AM > That's just an identifier, and there is an ASCII equivalent. Any user > could have done the same. NOT! They could not have done it in the standard library, and it has been a HUGE pain for us to accomodate this one special case. **************************************************************** From: Bob Duff Sent: Tuesday, November 17, 2009 8:20 AM > > Cool! Those look like upside-down A and backwards E on my screen! > > I've no idea how you typed them in. > > not on my screen :-) Now you've mailed them back to me, they look different. The for-all symbol looks like an 'a' with a '^' on top, followed by a '^', followed by a Euro symbol (three characters). And when Randy mailed them back to me, they both looked like '?'. Q.E.D. (that we shouldn't touch such characters with a barge pole) **************************************************************** From: Erhard Ploedereder Sent: Tuesday, November 17, 2009 3:19 AM RE: "for some" vs. "exists".... Is this a contest at all? Is there anybody who prefers "for some" to "exists"? (in boolean expressions) **************************************************************** From: Tucker Taft Sent: Tuesday, November 17, 2009 11:52 AM I think I prefer "for some" because it better suggests the loop involved. I am also somewhat swayed by the fact that "exists" will never fly as a reserved word, whereas I could imagine handling "for some" either by making "some" reserved, or by only reserving it in this context. **************************************************************** From: Bob Duff Sent: Tuesday, November 17, 2009 12:00 PM Same here. Also, I don't see any need to be overly mathematical in our notation. (E.g. I much prefer using the words "and" and "or" over the operators maths folks sometimes use -- even if those operators were part of 7-bit ascii and appeared on my keyboard.) But I'm not sure, because I haven't seen the exact BNF being proposed for 'exists'. By the way, some people are fanatically opposed to semi-reserved keywords. Not me. **************************************************************** From: Randy Brukardt Sent: Tuesday, November 17, 2009 12:06 PM > Is this a contest at all? Is there anybody who prefers "for some" to > "exists"? (in boolean expressions) I don't like either much. Moreover, "Exists" does not fly as a reserved word for me. I found a number of instances of parameters and variables named "Exists" in part of the Janus/Ada compiler (a small sample, but I think it is instructive): procedure Task_Guard(Exists : in Boolean); --- procedure Find_SYM (Current_Class : in out J2Typ_Decs.Library_Type; Line : in Target.Line_Numbers; Pos : in Target.Line_Position; Can_Create : in Boolean; Exists : out Boolean); --- Exists : Boolean; Can_Create => FALSE, Exists => Exists); if Exists then (There are two more instances like this in this package; these are all making calls on Find_SYM) --- Perhaps these would have been better named "File_Exists" or something like that (there are a *lot* of those in the Janus/Ada compiler), but I doubt that our code is atypical. Thus I think the incompatibility caused by "Exists" as a reserved word is unacceptable. --- I didn't try all of the compiler tools or any of our other code (as I did the looking with a simple text search). I tried a similar search for Some; I didn't find any declarations, but it's hard to tell because of the number of comments and larger identifiers containing the text "Some". We need a smarter tool for that. Presumably, the AdaCore experiment will give a more definitive answer. **************************************************************** From: Robed; D**R– Sent: Tuesday, November 17, 2009 12:09 PM > By the way, some people are fanatically opposed to semi-reserved > keywords. Not me. Not me either, but I don't like to allow them unless they appear in a position where the identifier could not occur reading left to right for some in x .. y loop for some x ... loop seems uncomfortable to me **************************************************************** From: Robert Dewar Sent: Tuesday, November 17, 2009 12:10 PM Note that if you tolerate semi-reserved keywords, exists is fine because you will always have an identifier after exists **************************************************************** From: Jean-Pierre Rosen Sent: Wednesday, November 18, 2009 1:48 AM > I tried a similar search for Some; I didn't find any declarations, but > it's hard to tell because of the number of comments and larger > identifiers containing the text "Some". We need a smarter tool for that. :-) Adacontrol's rule: check entities (all some, all exists); **************************************************************** From: Edmond Schonberg Sent: Wednesday, February 3, 2010 5:21 PM here is a more fleshed-out proposal. It may still depend on the new iterator machinery, but most of it stands on its own. I think we have to bite the bullet and introduce the keyword "exists". [This is version /02 - Editor.] **************************************************************** From: Randy Brukardt Sent: Wednesday, February 3, 2010 5:21 PM > here is a more fleshed-out proposal. It may still depend on the new > iterator machinery, but most of it stands on its own. > I think we have to bite the bullet and introduce the keyword > "exists". 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". Robert was going to look at this in the AdaCore test suite, but he never reported back. But in the absence of him reporting that our code here is unusual, I would have to be 100% against making "exists" a reserved word. Especially for something that I would use rarely. ... > !wording > Add in 2,9 a new keyword > exists 2.9 defines "reserved words", not "keywords" (that was the name of the unreserved identifiers that we dropped last time after substantial opposition). I've corrected this. > Add to 3.3 (19) a new constant > quantified_expression_parameter This is written as a syntax item, but in the grammar you give below, this is not defined. And in the for loop wording that you presumably are borrowing from, this is a defined term, not a syntax. I've fixed this consistently throughout the proposal. > 4.5.8 Quantified expressions The clause number needs to be 4.5.9, at least given the existing other AIs. Maybe we'll change that in the future. > quantified_expression ::= > (quantifier defining_identifier in domain | predicate) > > quantifier ::= for all | exists > > domain ::= discrete_subtype_definition | expression > predicate ::= boolean_expression I don't get why these things are indented randomly. The indentation of Ada syntax is significant. I made them all consistent, but you need to tell me if that is what you meant. > Static Semantics > > A quantified expression declares a > quantified_expression_parameter, whose subtype is defined by the > domain: This is a term, no underscores, and, as this is the defining occurrence, it needs to be surrounded by *stars*. > 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 > > 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. I think this is supposed to be a bulleted list, but there is no bullets to be seen. And the second one seems to have a punctuation shortage. > Name resolution rules > > The expected type of a quantified expression is the predefined type > Boolean More missing punctuation. > If the domain is an expression, it is expected to be of any type. > > Dynamic semantics > > 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 is 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 evalution > 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. Another bulleted list?? "Evalution". ... > 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. > > ed:ALL_AI05 schonberg$ This looks like your computer's command line prompt. How did it get in your e-mail? **************************************************************** From: Ed Schonberg Sent: Wednesday, February 3, 2010 9:43 PM > Randy, overworked editor. Thanks for the careful editing. I'll check about the presence of Exists in our sources. **************************************************************** From: Randy Brukardt Sent: Wednesday, February 3, 2010 10:42 PM For the record, I realized that I had forgotten to actually read most of it (I was focused on typos). When I went back and did that, I found more typos that I fixed, and also that you forgot to define the expected type of a "predicate". I fixed the latter by copying the wording for "condition". **************************************************************** From: Tucker Taft Sent: Wednesday, February 3, 2010 10:31 PM How about "(for'all X in ...)" and "(for'some X in ...)"? Or "(for-all X in ...)" and "(for-some X in ...)"? Both of these would allow "some" not to be a reserved word. I agree with Randy that "Exists" is simply too common of a name for functions. I know I have written "if Exists(X) then ..." many times in various Ada applications. We either need a way to have an unreserved keyword, or pick some other less common word. In terms of less common words to make reserved, we could use "for_all" and "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? **************************************************************** From: Edmond Schonberg Sent: Monday, February 22, 2010 8:20 PM No, you are right, my slip of the finger (was translating from the predicate for primality, one negation too many) **************************************************************** From: Steve Baird Sent: Monday, February 22, 2010 7:02 PM > The postcondition for a sorting routine on arrays with can be written: > > Post => (for all I:T in A'First .. A (T'Pred(A'Last)) | A (I) <= A > (T'Succ (I))) Am I right in assuming that you meant T'Pred (A'Last) as opposed to A (T'Pred (A'Last)) ? I'm also not sure about > The expected type of a quantified expression is the > predefined type Boolean. I think we want to replace this sentence with something that more closely follows the rule for a qualified expression. That is, say nothing about the expected type of a quantified expression (that, after all, is determined by its context) and instead add a static semantics rule along the lines of 4.7(3.1/3): The nominal subtype of a quantified_expression is the predefined type Boolean. It would seem oddly fitting to have some sort of parallel between quantified expressions and qualified expressions. Finally, do we need to state (in the dynamic semantics section) that the loop_parameter_specification is elaborated? See 5.5(9). **************************************************************** From: Randy Brukardt Sent: Monday, February 22, 2010 7:20 PM Shouldn't the type of the expression be the same as the type of the predicate? Otherwise you have some weird implicit conversion going on here, which might require a change of representation (if the encoding of the boolean types is different). Else I agree with the rest of your comments. **************************************************************** From: Edmond Schonberg Sent: Monday, February 22, 2010 8:24 PM >Am I right in assuming that you meant > T'Pred (A'Last) >as opposed to > A (T'Pred (A'Last)) >? No, I want A(A'Last -1), T is the index type. ... >It would seem oddly fitting to have some sort of parallel between >quantified expressions and qualified expressions. I don't know, I also see quantified expressions as conditions in an if-statement, for which we do state the expected type. That parallel does not work for me. >Finally, do we need to state (in the dynamic semantics section) that >the loop_parameter_specification is elaborated? See 5.5(9). Yes. in particular now that it can include some complex container-valued expression **************************************************************** From: Edmond Schonberg Sent: Monday, February 22, 2010 8:33 PM >>> The postcondition for a sorting routine on arrays with can be >>> written: >>> Post => (for all I:T in A'First .. A (T'Pred(A'Last)) | A (I) <= A >>> (T'Succ (I))) >> >> Am I right in assuming that you meant >> T'Pred (A'Last) >> as opposed to >> A (T'Pred (A'Last)) >> ? Indeed, you are right, this is the range for the index. **************************************************************** From: Steve Baird Sent: Monday, February 22, 2010 8:58 PM > Shouldn't the type of the expression be the same as the type of the > predicate? Otherwise you have some weird implicit conversion going on > here, which might require a change of representation (if the encoding > of the boolean types is different). I thought about this exact point and decided that I prefer Ed's proposed rule. The rule you propose would be somewhat more complex to specify and (probably) somewhat more complex to implement. The only benefit would be slightly more intuitive semantics in a case that nobody cares about. I say "slightly" because I have no problem thinking of (for all I in Some_Range | Some_Derived_Boolean_Type'(Foo (I))) as being equivalent to a call to a function with body Temp : Standard.Boolean := True; begin for I in Some_Range loop if Some_Derived_Boolean_Type'(Foo (I)) = False then Temp := False; exit; end if; end loop; return Temp; . On the other hand, I don't feel strongly about this. There are good arguments for the rule you suggest. Either way is ok with me. **************************************************************** From: Steve Baird Sent: Monday, February 22, 2010 9:41 PM >> It would seem oddly fitting to have some sort of parallel between >> quantified expressions and qualified expressions. > > I don't know, I also see quantified expressions as conditions in an > if-statement, for which we do state the expected type. That parallel > does not work for me. At the very least we should replace the proposed "is" rule with a "shall be" rule: The expected type of a quantified expression shall be the predefined type Boolean. Consider a bad construct such as X : Float := (for all I in ...); . We do not want to define the expected type of the quantified expression to be Boolean - that would conflict with the definition of expected type that is inherited from context (in this case, 3.3.1(4)). I think (but this would have to be checked - I'm not sure) that the rule I originally suggested would then follow as a consequence. Still, an expression whose type is known independently of the context in which it occurs strikes me as being very similar to a qualified expression and I think it would be clearest to follow that example. **************************************************************** From: Edmond Schonberg Sent: Monday, February 22, 2010 9:51 PM ... >At the very least we should replace the proposed "is" rule with a >"shall be" rule: > The expected type of a quantified expression shall be the > predefined type Boolean. or "any boolean type" as for conditions in if-statements. ... >Still, an expression whose type is known independently of the context >in which it occurs strikes me as being very similar to a qualified >expression and I think it would be clearest to follow that example. Not sure I follow, this is the same phrasing as for conditions in if-statements, and those are not qualified expressions. Of course, those conditions are in one specific context, while quantified expressions are just expressions that can appear anywhere. So whatever is clearer. Still, the expected type of the predicate must be the same as that of the expression as a whole. **************************************************************** From: Randy Brukardt Sent: Monday, February 22, 2010 10:10 PM >Not sure I follow, this is the same phrasing as for conditions in >if-statements, and those are not qualified expressions. Steve is right. An if-statement is a context that *provides* an expected type. Kinds of expressions are defined to match certain expected types, they don't have them >Of course, those conditions are in one specific context, while >quantified expressions are just expressions that can appear anywhere. >So whatever is clearer. Still, the expected type of the predicate must >be the same as that of the expression as a whole. I had suggested that, and Steve thought it was better that quantified expressions always returned type Boolean. I don't think it matters that much. Steve now seems to be suggesting a resolution rule like that of qualified expressions: A quantified_expression shall resolve to type Boolean. But this is a bit different than regular resolution, as it doesn't include implicit conversions. Not sure that matters in this case (I can't think of a reason). An alternative would be to have a legality rule: The expected type of a quantified_expression shall be a boolean type. Not sure that works, though, so probably following the model of qualified expressions is better. Note that we might want the equivalent of the 4.7(3.1/3) rule, which specifies the nominal subtype. But since we didn't do that for conditional or case expressions (and I really don't want to go there!), maybe we don't need it here, either. (But note that 4.7(3.1/3) has nothing to do with resolution; we definitely need *some* rule about the resolution of a quantified_expression.) **************************************************************** From: Steve Baird Sent: Monday, February 22, 2010 10:21 PM >> At the very least we should replace the proposed "is" rule with a >> "shall be" rule: >> The expected type of a quantified expression shall be the >> predefined type Boolean. > > or "any boolean type" as for conditions in if-statements. That would be fine too. As I mentioned in an earlier reply to Randy, I prefer your original rule but I don't feel strongly about it. ... >> Still, an expression whose type is known independently of the context >> in which it occurs strikes me as being very similar to a qualified >> expression and I think it would be clearest to follow that example. >> > Not sure I follow, this is the same phrasing as for conditions in > if-statements, and those are not qualified expressions. I was just repeating myself, stating that the proposed "shall be" wording is my second choice; I still prefer The nominal subtype of a quantified_expression is the predefined type Boolean. On the other hand, if we adopt the "any boolean type" rule that you mentioned above, then the parallel with qualified expressions falls apart (the type of a quantified expression could no longer be determined independently of its context). In that case, I think the "shall be" wording would be best. > So whatever is clearer. Agreed. Let's see what others think. **************************************************************** From: Randy Brukardt Sent: Monday, February 22, 2010 10:40 PM > Corrected text follows. I changed the example again, as you forgot to change 1 to 2 in the loop. Moreover, everytime I read the leadin "The assertion that a positive number is composite can be written:" I think the answer is "False" (because "composite" has a meaning in Ada, and a number is never composite in Ada). I changed it to: The assertion that a positive number is composite (as opposed to prime) can be written: So as to avoid confusion for Ada-lawyer readers. --- You changed the resolution rule to: The expected type of a quantified expression is any Boolean type. The predicate in a quantified_expression is expected to be the same type. This is completely backwards. As Steve says, expected types always come from context. Moreover, not all expressions have expected types at all (qualified expressions don't, for instance). So it is dangerous to talk about the expected type of the expression. (We fought this for conditional_expressions; we eventually used the rules that () would have if they actually had rules.) We could use similar rules here: If a quantified_expression is expected to be of a type T, the expected type for each *dependent_*expression of the quantified_expression is T. If a quantified_expression shall resolve to a type T, each dependent_expression shall resolve to T. And then we'd need a legality rule: The type of a quantified_expresion shall be a boolean type. Alternatively, we could follow Steve's suggestion. However, that is unfortunate as the only place the type (as opposed to the subtype, and we just added that very recently) of a qualified_expression is defined is in the informal introductory text. (Ignore my previous message on this subject.) So there isn't a good example to copy. Aside: We didn't try to identify the type of a conditional expression, much less the subtype. So what is the completeness rule for a case statement? Consider: case (if Func then 1 else 2) is when 1 => null; when 2 => null; end case; Is an others required or not?? Same applies to a case_expression. (Darn, I'm thinking like Steve now.) **************************************************************** From: Bob Duff Sent: Tuesday, February 23, 2010 7:33 PM > Steve is right. An if-statement is a context that *provides* an > expected type. Kinds of expressions are defined to match certain > expected types, they don't have them I don't "get" this tempest in a tea pot. Just define the doggone result type! The expected type for the predicate is "any boolean type". The type of a quantified_expression is Boolean. Word it that way: end of story, no? I don't get what various folks are arguing about (just wording?). There's no need to define "expected type" for quantified_expression; indeed that makes no sense, as Randy explains above. Expected types go down, result types go up (assuming you draw trees with roots at the top and leaves at the bottom, like all right-thinking computer scientists do). Maybe I'm missing something... By the way, there's a bit of a notational problem here: quantified_expression ::= (for quantifier loop_parameter_specification | predicate) quantifier ::= all | some predicate ::= boolean_expression There's an ambiguity about what "|" means (and it threw me for a loop at first!). "1.1.4 Method of Description and Syntax Notation" contains this kludge: 12 * A vertical line separates alternative items unless it occurs immediately after an opening curly bracket, in which case it stands for itself: 13 constraint ::= scalar_constraint | composite_constraint discrete_choice_list ::= discrete_choice {| discrete_choice} Sigh. Oh what a tangled web we weave, when first we practise to kludge. Apologies to Scott, whose version rhymes better, but my version is apt. I shall refrain from suggesting that "such" and "that" should be keywords, reserved or otherwise. **************************************************************** From: Edmond Schonberg Sent: Wednesday, February 24, 2010 1:17 PM > By the way, there's a bit of a notational problem here: > > quantified_expression ::= (for quantifier > loop_parameter_specification | predicate) > quantifier ::= all | some > predicate ::= boolean_expression > > There's an ambiguity about what "|" means (and it threw me for a loop > at first!). Yes, sorry for the sloppy notation. The vertical bar should be in quotes... or else we choose a different separator: colon and right-arrow have been proposed: for all X in S : P (X) or for all X in S => P (X) Slight preference for colon in this context, but that would conflict with the new iterator syntax, where we could say: for all X : T of C : P (X) which is definitely confusing. So right arrow may be the obvious choice. **************************************************************** From: Bob Duff Sent: Wednesday, February 24, 2010 1:39 PM > Yes, sorry for the sloppy notation. The vertical bar should be in > quotes... The first one. > or else we choose a different separator: colon and right-arrow have > been proposed: > > for all X in S : P (X) > > or > > for all X in S => P (X) > > Slight preference for colon in this context, but that would conflict > with the new iterator syntax, where we could say: > > for all X : T of C : P (X) > > which is definitely confusing. So right arrow may be the obvious > choice. Well, I hate for our inability to say "|" in our meta-language drive the actual syntax. Anyway, I agree ":" is confusing. I could live with either "=>" or "|". Maybe we should change "1.1.4 Method of Description and Syntax Notation" to say that "|" (with the quotes) stands for a vertical line, and change the syntax for discrete_choice_list, discriminant_association, component_choice_list, and exception_handler to quote the thing? (If I ran the circus, all literal terminals would be quoted.) **************************************************************** From: Gary Dismukes Sent: Wednesday, February 24, 2010 1:55 PM > Yes, sorry for the sloppy notation. The vertical bar should be in > quotes... > or else we choose a different separator: colon and right-arrow have > been proposed: Just because there's a notational issue with the syntax doesn't mean we should change to a different separator. Let's please stick with the vertical bar and resolve the syntax notation issue somehow. **************************************************************** From: Tucker Taft Sent: Wednesday, February 24, 2010 2:04 PM I agree. "|" seems preferable to other separators. In other places where we use "|" in the syntax (e.g. 4.3.1 record aggregates), the distinction seems to be merely one of the font (which is admittedly pretty subtle). **************************************************************** From: Edmond Schonberg Sent: Wednesday, February 24, 2010 2:05 PM > Just because there's a notational issue with the syntax doesn't mean > we should change to a different separator. Let's please stick with > the vertical bar and resolve the syntax notation issue somehow. I wasn't suggesting the other possible separators just because of the notational issue. I've heard objections (on aesthetic grounds) about the use of the vertical bar here (from John in particular), and other had suggested => as more meaningful. **************************************************************** From: Randy Brukardt Sent: Wednesday, February 24, 2010 7:59 PM > I agree. "|" seems preferable to other separators. > > In other places where we use "|" in the syntax (e.g. 4.3.1 record > aggregates), the distinction seems to be merely one of the font (which > is admittedly pretty subtle). All such cases follow "{", and the wording that Bob pointed out covers that explicitly. This is the first time | is used to separate something other than a list, so now we have a problem. No solution comes to mind. (One also wonders about the inconsistency of using a list separator in a non-list context. I'd solve the problem by not bothering with this feature, but I'm not expecting that solution to fly. :-) **************************************************************** From: Steve Baird Sent: Wednesday, February 24, 2010 1:26 PM > I don't get what various folks are arguing about (just wording?). Pretty much. There is a more-than-just-wording question about a corner case which nobody seems to feel strongly about, but which needs to be resolved one way or the other: If the predicate expression is of a derived boolean type, is the type of the quantified expression Standard.Boolean or is it the derived boolean type? I argued that if we choose Standard.Boolean, then a quantified expression is a lot like a qualified expression in the sense that its type can be determined independently of its context. This suggested to me that we should therefore use the wording for qualified expressions as a model. Unfortunately, this introduced confusion because, as Randy pointed out, the wording for qualified expressions isn't really right. It hasn't changed for many years and there have been no complaints about it, but doesn't explicitly define the type of a qualified expression. It does define the nominal subtype, but Randy says that "4.7(3.1/3) has nothing to do with resolution,". So something like The type of a quantified_expression is the predefined type Boolean. is probably needed. If we go the other way on the derived-boolean-type corner-case question, then of course things are different. **************************************************************** From: Edmond Schonberg Sent: Wednesday, February 24, 2010 1:42 PM > So something like > The type of a quantified_expression is the predefined type Boolean. > is probably needed. That's certainly the simplest. I see zero advantage in saying "any boolean type" here (or elsewhere for that matter...). **************************************************************** From: Bob Duff Sent: Wednesday, February 24, 2010 1:44 PM > If the predicate expression is of a derived boolean type, is > the type of the quantified expression Standard.Boolean or is > it the derived boolean type? I see. The correct answer is "Who cares?", but I agree we need to decide one way or 'tother. ... > So something like > The type of a quantified_expression is the predefined > type Boolean. > is probably needed. OK with me. It does mean that Interfaces.Fortran.Logical gets implicitly converted to Boolean, which involves a change of representation. Problem? **************************************************************** From: Tucker Taft Sent: Wednesday, February 24, 2010 1:57 PM I think I disagree with saying it is the predefined type Boolean, on language consistency grounds. Standard.Boolean appears essentially nowhere in the name resolutions rules, so why introduce it here? Since conditions are allowed to be of any boolean type, then I would say the expected type for the predicate expression is "any boolean type", and the type of the quantified expression is the same as that of the predicate expression. In fact, if you define "predicate" as: predicate ::= condition then I think much of this happens for free, since "condition" is already defined in RM 5.3 to have an expected type of "any boolean type." **************************************************************** From: Bob Duff Sent: Wednesday, February 24, 2010 2:15 PM > I think I disagree with saying it is the predefined type Boolean, on > language consistency grounds. > Standard.Boolean appears essentially nowhere in the name resolutions > rules, so why introduce it here? I think I agree with Tucker here. > Since conditions are allowed to be of any boolean type, then I would > say the expected type for the predicate expression is "any boolean > type", ... Yes, definitely -- that's the way everything else works, so should be easiest to implement. That's what I suggested before. >...and the type of the quantified > expression is the same as that of the predicate expression. Yes, I've changed my mind, and now agree it should not be hardwired to Boolean. I actually think this is easier to implement, because you don't have to implicitly convert from Derived_Boolean to Boolean (which could require a change of representation). >...In fact, if you define "predicate" as: > > predicate ::= condition > > then I think much of this happens for free, since "condition" is > already defined in RM 5.3 to have an expected type of "any boolean > type." Good idea. This covers the expected type of the predicate. We still need to say that the type of the quant_exp is that of the predicate. **************************************************************** From: Bob Duff Sent: Wednesday, February 24, 2010 2:18 PM > That's certainly the simplest. I see zero advantage in saying "any > boolean type" here (or elsewhere for that matter...). Perhaps, but we already do so elsewhere, so it's simplest to do likewise here. Anyway, it's kind of convenient to be able to use if statements on type Interfaces.Fortran.Logical. **************************************************************** From: Tucker Taft Sent: Wednesday, February 24, 2010 2:55 PM Is this Bob Duff I or Bob Duff II? I thought you just sent out a note agreeing the predicate should be expected to be of any boolean type, and the quantified expression should be that same type. Implicit converting to Standard.Boolean seems of little value, and if someone has gone to the effort of using a non-standard boolean type, they would presumably be annoyed that all of the logical operations preserve their non-standard boolean type *except* quantified expressions. **************************************************************** From: Randy Brukardt Sent: Wednesday, February 24, 2010 3:05 PM Some of Bob's messages got delivered out of order because they were briefly delayed in the spam filter. That might account for the confusion. **************************************************************** From: Edmond Schonberg Sent: Wednesday, February 24, 2010 3:14 PM > Implicit converting to Standard.Boolean seems of little value, and if someone > has gone to the effort of using a non-standard boolean type, they would > presumably be annoyed that all of the logical operations preserve their > non-standard boolean type *except* quantified expressions. the argument about Fortran.Logical seems compelling, so I agree that these should be treated like other conditions. "Any boolean type"is fine. **************************************************************** From: Steve Baird Sent: Wednesday, February 24, 2010 3:29 PM > I see. The correct answer is "Who cares?", but I agree we need to > decide one way or 'tother. Agreed. >> So something like >> The type of a quantified_expression is the predefined >> type Boolean. >> is probably needed. > > OK with me. It does mean that Interfaces.Fortran.Logical gets > implicitly converted to Boolean, which involves a change of > representation. Problem? I don't see it as a problem, although it sounds like it doesn't matter whether it is a problem or not because folks seem to be leaning towards the "use the type of the predicate" approach (which is fine with me). One could even argue that there isn't any change of representation (or at least it is well camouflaged) if you choose to think of a quantified expression as I described it in an earlier message: > ... I have no problem thinking of > > (for all I in Some_Range | Some_Derived_Boolean_Type'(Foo (I))) > > as being equivalent to a call to a function with body > > Temp : Standard.Boolean := True; > begin > for I in Some_Range loop > if Some_Derived_Boolean_Type'(Foo (I)) = False then > Temp := False; > exit; > end if; > end loop; > return Temp; **************************************************************** From: Bob Duff Sent: Wednesday, February 24, 2010 3:35 PM > Is this Bob Duff I or Bob Duff II? > I thought you just sent out a note agreeing the predicate should be > expected to be of any boolean type, and the quantified expression > should be that same type. I think you read my e-mails in the opposite order I sent them. I changed my mind. My current opinion agrees with yours. Reasons: Easier to implement. Better for the user of derived types (not many of those, but we do have Logical). **************************************************************** From: Bob Duff Sent: Wednesday, February 24, 2010 8:19 PM > All such cases follow "{", and the wording that Bob pointed out covers > that explicitly. This is the first time | is used to separate > something other than a list, so now we have a problem. Right. >...No solution comes to mind. I suggested one. Quote the | and say so in section 2.whatever. >... (One also > wonders about the inconsistency of using a list separator in a >non-list context. I'm happy with either "=>" or "|". I don't understand why Gary adamantly prefers the latter. Shrug. >... I'd solve the problem by not bothering with this feature, but I'm >not expecting that solution to fly. :-) Well, it's easy to implement (my main concern)... **************************************************************** From: Jean-Pierre Rosen Sent: Thursday, February 25, 2010 3:53 AM > Since conditions are allowed to be of any boolean type, then I would > say the expected type for the predicate expression is "any boolean > type", Agreed, and the argument for Logical is important for this one. > and the type of the quantified > expression is the same as that of the predicate expression. I don't see any reason why the result type of the quantified expression should be the same as the type of the predicate. After all, if I write: L : Fortran.Logical; ... if L = True then The type of "=" is Boolean, not logical. I see the predicate as a kind of "extended" equality. Why should it be different? **************************************************************** From: Tucker Taft Sent: Thursday, February 25, 2010 8:10 AM Really? I see it as an extended "and then" or "or else". **************************************************************** From: Jean-Pierre Rosen Sent: Thursday, February 25, 2010 8:23 AM Interesting. To me, it answers the question: "Is it true that all Foos verify this condition?" rather than an "and then" between the evaluation of all the conditions. **************************************************************** From: Edmond Schonberg Sent: Thursday, February 25, 2010 8:32 AM The dynamic semantics makes it clear that the evaluation is short-circuited (stop when counterexample is found) so this is definitely a sequence of "and then" between conditions. **************************************************************** From: Jean-Pierre Rosen Sent: Thursday, February 25, 2010 8:49 AM Sure - and nobody even thought of not stopping as soon as the result is known. But that it is implementation. From a user's point of view, I would say that this is a predicate. The same way you ask "is X equal to 1?" you would ask "are all elements of Tab equal to 1?". All comparison operators return boolean... **************************************************************** From: Bob Duff Sent: Thursday, February 25, 2010 9:15 AM I don't see that, because "are all elements of Tab equal to 1?" would be: (for all I in Some_Range | Foo (I) = 1) and that will return Boolean under either rule we're arguing about, because "Foo (I) = 1" is Boolean. The only issue would be if the predicate were actually of type Logical (or some other derived type). For example, if you have an array A of Logical, and say: (for all I in Some_Range | A (I)) It seems to me the result should be Logical. You are arguing for Steve's point of view, here: > ... I have no problem thinking of > > (for all I in Some_Range | Some_Derived_Boolean_Type'(Foo (I))) > > as being equivalent to a call to a function with body > > Temp : Standard.Boolean := True; > begin > for I in Some_Range loop > if Some_Derived_Boolean_Type'(Foo (I)) = False then > Temp := False; > exit; > end if; > end loop; > return Temp; But Steve's code could just as well be: > Temp : Some_Derived_Boolean_Type := True; <<<<< > begin > for I in Some_Range loop > if not Some_Derived_Boolean_Type'(Foo (I)) then <<<<< > Temp := False; > exit; > end if; > end loop; > return Temp; (Modified lines marked <<<<<.) I find the latter more intuitive, because I always write "if not Blah" rather than "if Blah = False". **************************************************************** From: Edmond Schonberg Sent: Thursday, February 25, 2010 8:18 AM The update of AI-0176 seems incomplete. The version I sent a few days ago uses the new iterator forms, and the non-reserved keyword "for some" not "exists". **************************************************************** From: Randy Brukardt Sent: Thursday, February 25, 2010 12:02 PM Not sure what you are looking at. The version posted on the web (version /04) has all of those changes. **************************************************************** From: Edmond Schonberg Sent: Thursday, February 25, 2010 7:15 PM Looking at the one on the web. The productions (under 4.5.9) are old, they mention "exists" and do not mention the new iterator forms (using 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) **************************************************************** From: Christoph Grein Sent: Monday, June 14, 2010 4:25 AM 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 the sentence above. 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". **************************************************************** 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 > meaning and effects {of} this Rule. > > 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 to the *real* 4.5.7. But we hadn't approved AI-147 yet, so it isn't included in the 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 > of "all". Probably a good idea. **************************************************************** From: Bob Duff Sent: Thursday, July 8, 2010 2:31 PM Minor comments on the Quantified expressions AI: > Quantified expressions have the following syntax: > > ( for quantifier loop_parameter_specification | > Boolean_Expression ) > 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.] "Some" is a keyword, and should appear in lowercase boldface when used as such. It would be a reserved word, except for compatibility. Programmers will do just fine if they think of it as a reserved word. It really looks silly to format "for all" and "for some" in two different styles! There should be another NOTE before 2.9(3), something like: The keyword "some" is used in the syntax of quantified_expressions (see 4.5.9), but it is not reserved. If there are others (I don't remember any), it could be: The following keywords are used in the syntax, but are not reserved: "some", "mumble", "bumble", "dumble". The existing NOTE 2.9(3) should be modified: 3 8 Keywords appear in lower case boldface in this International Standard, except when used in the designator of an attribute (see 4.1.4). Lower case boldface is also used for a reserved word in a string_literal used as an operator_symbol. This is merely a convention - programs may be written in whatever typeface is desired and available. No need to formally define "keyword" -- these are just NOTEs, and it's clear enough what it means from the new NOTE I suggested. I don't understand when parens are required around quantified_expressions, nor how the syntax rules specify that. The first sentence quoted above shows parens, but I don't see them in the syntax rules. In the formatted version, the three syntax rules appear all on one line, and are therefore undecipherable. The above quote is from the unformatted version. This AI is already ARG approved. If my comments above are not controversial then I think they can be considered as editorial changes. If they ARE controversial, then I'll start pounding my shoe on the table. ;-) **************************************************************** From: John Barnes Sent: Thursday, July 8, 2010 2:42 PM The WG9 meeting in Valencia sent back AI-176 and directed the ARG to make some a reserved word. Accordingly it was made a reserved word at the immediately following ARG meeting. **************************************************************** From: Bob Duff Sent: Thursday, July 8, 2010 3:04 PM Ah, thanks for the info. I was looking at the latest online version of the AI, which has not been updated since the recent meeting. I'm not surprised by this change. During Ada 9X, we proposed to have nonreserved keywords, and some folks were rabidly opposed to the concept. I seem to recall Robert Dewar was one of those. Either I'm misremembering, or he has changed his mind, because he's OK with it now. I don't really get it -- it seems to me the very practical concern of compatibility ought to trump some minor aesthetic unease about the concept of nonreserved keywords. And using Until as a variable name doesn't cause any real confusion with "delay until 1.0;" -- no more than using Queue as a user-defined type, now that Queue is a predefined type. **************************************************************** From: Stephen Michell Sent: Thursday, July 8, 2010 3:20 PM Agreed. "some" is now a reserved word. **************************************************************** From: Randy Brukardt Sent: Friday, July 9, 2010 12:55 PM > I'm not surprised by this change. During Ada 9X, we proposed to have > nonreserved keywords, and some folks were rabidly opposed to the > concept. > I seem to recall Robert Dewar was one of those. Either I'm > misremembering, or he has changed his mind, because he's OK with it > now. We also tried it with "interface" for Ada 2005, because of the conflict with pragma Interface. That was also rejected. So we're 0-3 on this one. > I don't really get it -- it seems to me the very practical concern of > compatibility ought to trump some minor aesthetic unease about the > concept of nonreserved keywords. And using Until as a variable name > doesn't cause any real confusion with "delay until 1.0;" -- no more > than using Queue as a user-defined type, now that Queue is a > predefined type. Well, WG 9 votes by countries. The US delegation (which is a significant fraction of the ARG) was strongly in favor of unreserved keywords. All of the rest of the world voted against them (I don't think the feeling was as strong for most countries, but it was for a few). That's why this continually comes up: this the rare case where by-country voting (as in WG 9) and pluralities (as in the ARG) get different answers. To change this result, some of us need to move to Canada or France. ;-) **************************************************************** From: Robert Dewar Sent: Friday, July 9, 2010 1:02 PM > I seem to recall Robert Dewar was one of those. Either I'm > misremembering, or he has changed his mind, because he's OK with it > now. I am never rapidly against anything, frankly I wuld prefer this time around to make SOME non-reserved, since I dislike gratuitous incoimpatibilities, but it's not a big deal either way. I am happy to make it reserved. **************************************************************** From: Bob Duff Sent: Friday, July 9, 2010 1:30 PM > I am never rapidly against anything, ... Maybe you used the word "rubbish" during the argument -- I don't remember. ;-) Interesting typo, by the way. >...frankly I wuld prefer > this time around to make SOME non-reserved, since I dislike >gratuitous incoimpatibilities, but it's not a big deal either way. I >am happy to make it reserved. Yes, I agree 100% with all that. I'd say the same about "interface" and "until". **************************************************************** From: Robert Dewar Sent: Friday, July 9, 2010 1:50 PM >> I am never rapidly against anything, ... > > Maybe you used the word "rubbish" during the argument -- I don't > remember. ;-) rabid seems to be about being angry or emotional, when I call something rubbish, it conveys neither, just technical disapproval. > Interesting typo, by the way. > >> ...frankly I wuld prefer >> this time around to make SOME non-reserved, since I dislike >> gratuitous incoimpatibilities, but it's not a big deal either way. I >> am happy to make it reserved. > > Yes, I agree 100% with all that. I'd say the same about "interface" > and "until". Oh well! The ARG-WG9 community is not attuned enough to the pain of non-upwards compatibility, they seem to think that any source in the world can be fed through SED :-) **************************************************************** From: Bob Duff Sent: Friday, July 9, 2010 2:31 PM > rabid seems to be about being angry or emotional, when I call > something rubbish, it conveys neither, just technical disapproval. I'm not sure if you took "rabid" as an insult or not, but just in case you did, I apologize! **************************************************************** From: Robert Dewar Sent: Friday, July 9, 2010 3:11 PM It is impossible to insult me in a technical argument, I never get emotional over technical stuff, it is too unimportant for that :-) I like energetic argument, but it's never quarrelling for me :-) So, no need to apologize. **************************************************************** From: Yannick Moy Sent: Wednesday, July 7, 2010 6:06 AM I'd like to emphasize the need for cursor ranges for expressing quantified properties over containers, in particular for "loop invariants" (even if Ada does not define such a notion) on loops which iterate over containers. Say a loop iterates over a set to increment its values: Cont : Set; Cur : Cursor := First (Cont); begin while Has_Element (Cur) loop pragma Assert (for all X in Cont range First (Cont) .. Previous (Cur) | X = X'Old + 1); pragma Assert (for all X in Cont range Cur .. Last (Cont) | X = X'Old); Replace_Element (Cont, Cur, Element (Cur) + 1); end loop; I have written in assertions the loop invariant property of this loop, namely that all previous elements have been incremented and all following elements are the same. With ordered sets, it would be possible to express the same properties with comparisons between cursors, but then X is not a cursor, plus it would not be possible with hashed sets since they don't define comparison between cursors. Do you see an alternative way of expressing the same properties? If not, does it seem reasonable to include ranges over container cursors? **************************************************************** From: Randy Brukardt Sent: Wednesday, July 7, 2010 11:03 AM > I'd like to emphasize the need for cursor ranges for expressing > quantified properties over containers, in particular for "loop > invariants" (even if Ada does not define such a notion) on loops which > iterate over containers. Keep in mind that there are two forms of iterators for use with containers, one using an explicit cursor and one just providing the elements. If you need to have a cursor for some reason (including to write Asserts), I think it is reasonable to require using the first form. The element form is just a shorthand anyway, and is never necessary. To write your example as a for loop (or as quantified expression), use the cursor form: for Cur in Iterator(Cont) loop pragma Assert (for all X in Cont range First (Cont) .. Previous (Cur) | X = X'Old + 1); pragma Assert (for all X in Cont range Cur .. Last (Cont) | X = X'Old); Replace_Element (Cont, Cur, Element (Cur) + 1); end loop; ... > With ordered sets, it would be possible to express the same properties > with comparisons between cursors, but then X is not a cursor, plus it > would not be possible with hashed sets since they don't define > comparison between cursors. It doesn't make sense to talk about a "range" in the hashed containers. What would it mean? The order of the elements depends on the hash function and the size of the hash table and the implementation and thus is essentially unpredictable. It only makes sense to iterate on the entire set of elements for one of the hashed forms. For the other forms, there probably will be ranged iterators available: for Cur in Range_Iterator (Cont, Start => First, Finish => Last) loop ... which of course will just iterate part of the container. The advantage to the full form of iterators is that since they are returned by a function, that function can have as many parameters as necessary to define the iteration. **************************************************************** From: Yannick Moy Sent: Thursday, July 8, 2010 2:07 AM > Keep in mind that there are two forms of iterators for use with > containers, one using an explicit cursor and one just providing the > elements. If you need to have a cursor for some reason (including to > write Asserts), I think it is reasonable to require using the first > form. The element form is just a shorthand anyway, and is never necessary. ... The problem I mentioned was about the quantification in the assertion, which is always over elements of the container, not cursors, as currently described in AI05-0176-1. So you cannot write: pragma Assert (for all X in Cont | if First (Cont) <= X and X <= Previous (Cur) then X = X'Old + 1); And since ranges over cursors are not allowed either: pragma Assert (for all X in Cont range First (Cont) .. Previous (Cur) | X = X'Old + 1); then, there is no way apparently to express the property "all elements before the cursor Cur have been incremented". > It doesn't make sense to talk about a "range" in the hashed > containers. What would it mean? The order of the elements depends on > the hash function and the size of the hash table and the > implementation and thus is essentially unpredictable. It only makes > sense to iterate on the entire set of elements for one of the hashed forms. Right, but during iteration you still have "those elements which have been processed" and "those elements which have not", which correspond to the cursors "before" and "following" the current cursor. How do you express the property above ("all elements before the cursor Cur have been incremented") when iterating over a hashed set? > For the other forms, there probably will be ranged iterators available: > > for Cur in Range_Iterator (Cont, Start => First, Finish => Last) loop > ... > > which of course will just iterate part of the container. The advantage > to the full form of iterators is that since they are returned by a > function, that function can have as many parameters as necessary to > define the iteration. Interesting, but this only applies to loops, right? What about quantification on containers in expressions, as described by AI05-0176-1? **************************************************************** From: Randy Brukardt Sent: Friday, July 9, 2010 12:47 PM > The problem I mentioned was about the quantification in the assertion, > which is always over elements of the container, not cursors, as > currently described in AI05-0176-1. So you cannot write: > > pragma Assert (for all X in Cont | > if First (Cont) <= X and X <= Previous (Cur) > then X = X'Old + 1); I had thought the intent was that all of the iterator forms would be supported in quantified expressions, but it is clear that the current AI does not do that. I think you have demonstrated why the cursor forms are needed in quantified expressions, so we ought to revisit that. > > It doesn't make sense to talk about a "range" in the hashed > > containers. What would it mean? The order of the elements depends on > > the hash function and the size of the hash table and the > > implementation and thus is essentially unpredictable. It only makes > > sense to iterate on the entire set of elements for one of > the hashed forms. > > Right, but during iteration you still have "those elements which have > been processed" and "those elements which have not", which correspond > to the cursors "before" and "following" the current cursor. How do you > express the property above ("all elements before the cursor Cur have > been > incremented") when iterating over a hashed set? I don't think you can, and I'm not sure it makes sense to do so. Cursors in a hashed set have no order, and there is no reason to assume that the order selected for a particular iterator can even be reproduced (a later iterator may use a different order). Any dependence on ordering is bogus. Why don't you just check that all of the elements are processed after the loop completes? It would be cheaper (the check you propose is quadratic) and would have the same effect. ... > Interesting, but this only applies to loops, right? What about > quantification on containers in expressions, as described by > AI05-0176-1? Quantifiers need the cursor forms, for this reason and the others you noted. That ought to be fixed. After all, the cursor forms are the more general ones, and limiting only to the less general forms always is going to lead to trouble. **************************************************************** From: Bob Duff Sent: Friday, July 9, 2010 1:25 PM > Why don't you just check that all of the elements are processed after > the loop completes? It would be cheaper (the check you propose is > quadratic) and would have the same effect. I suspect Yannick is thinking about static proofs here. Yeah, you'd have an assertion after the loop (or a postcondition on the procedure). You're trying to deduce that that's True, from the loop invariant ("all the ones done so far have so-and-so property"), plus the exit condition ("the ones done so far = all of them"). And you deduce the loop invariant inductively (if it was True last time around, then it must be True this time). This sort of reasoning doesn't care that hash tables iterate in an arbitrary order. **************************************************************** From: Randy Brukardt Sent: Friday, July 9, 2010 1:49 PM Right, but it does require that the order to reproducible, and there is no such requirement on the hashed containers at this point. The only requirement is that each item is touched only once for a particular iterator instance. A perfectly acceptable implementation would have a list of items yet to be processed stored as part of the iterator; the container itself may not have any knowledge of the order of operations and surely will not know the state of the iterator (iterator objects being separate from the container for the new iterators, and the information being stored in the locals of the subprogram for the existing passive iterators). In order to say anything about the order (such as having functions to query whether or not an item is already processed), the container has to know the order and keep it unchanged so long as any one can reasonably ask about it. That seems like a significant impact on the design of what is supposed to be an unordered container. I would think that static proofs for unordered iterators have to be done on the loop as a whole (not on intermediate positions). That is, there has to be a proof that all of the iterations complete (no exceptions raised, etc.) and that each iteration has the intended effect on its single element. I realize that's easier said than done. But the sort of loop invariants that Yannick is talking about don't make sense in the absence of a defined order, and aren't really necessary for whole container iterators unless there is an intent that the loop not complete all of the iterations. That is, if the intent is that the loop operate on the entire container without interruption, there is no need to have loop invariants that say anything about elements other than the current one. (That job ought to be done by an assertion or the like after the loop.) **************************************************************** From: Bob Duff Sent: Friday, July 9, 2010 2:28 PM > Right, but it does require that the order to reproducible, and there > is no such requirement on the hashed containers at this point. Good point -- I didn't think of that! Perhaps there should be. That is, if you iterate twice over the same container, and it hasn't changed, then the iterations happen in the same order (but that order is arbitrary). By "change", I mean adding/inserting/moving elements -- modifying the content of elements doesn't count. I can't imagine any sensible implementation of hash tables that would violate this rule, and it seems somewhat useful. If you insert an element into the hash table, that can of course radically alter the order of subsequenct iterations. **************************************************************** From: Tucker Taft Sent: Friday, July 9, 2010 2:42 PM All of the iterator forms should be included in the quantified expr. This was probably just an oversight. **************************************************************** From: Yannick Moy Sent: Monday, July 12, 2010 2:41 AM >> Right, but it does require that the order to reproducible, and there >> is no such requirement on the hashed containers at this point. > > Good point -- I didn't think of that! > > Perhaps there should be. That is, if you iterate twice over the same > container, and it hasn't changed, then the iterations happen in the > same order (but that order is arbitrary). > By "change", I mean adding/inserting/moving elements -- modifying the > content of elements doesn't count. That would be terribly useful for static verification. As you correctly guessed in a previous email, I am concerned with the ability to express loop invariants for static verification. These are properties that are maintained throughout the loop and which usually describe the intermediate state of the container during iteration. So there must be a way to describe those elements which have been treated and those elements which have not. It is not sufficient to describe the result of the loop after a complete execution: it will be possible to test it during execution, but this will not be provable statically without a loop invariant as described above. > I can't imagine any sensible implementation of hash tables that would > violate this rule, and it seems somewhat useful. In order to have properties that are used both for dynamic and static verification, this is very useful. > If you insert an element into the hash table, that can of course > radically alter the order of subsequenct iterations. agreed, no problem with that. **************************************************************** From: Randy Brukardt Sent: Monday, July 26, 2010 9:12 PM > All of the iterator forms should be included in the > quantified expr. This was probably just an oversight. For the record, I've fixed up the draft version of AI05-0176-1 to reference all of the new syntax proposed in AI05-0139-2. I believe that will be sufficient to include all of the iterator forms. **************************************************************** From: John Barnes Sent: Wednesday, September 15, 2010 10:10 AM I am usually reasonably placid over the changes proposed to Ada but I keep finding my blood pressure raised by quantified expressions. This has struck me twice in the past few days, once when reviewing AI-176 and now again when reviewing the parts of the RM that I have been allocated. I very strongly object to using the vertical bar to introduce the predicate as in (using the examples in the RM) for all I in A'First .. T'Pred(A'Last) | A(I) <= A(T'Succ(I)) pragma Assert(for some X in 2 .. N/2 | N mod X = 0); There are several things I don't like * it complicates the vertical bar rules in 1.1.4. It's bad enough that we have a problem here anyway dating back to Ada 83 with the "following a curly brace rule" but to make matters so much worse seems criminal to me. In any event at least the curly brace rule is more of a punctuation thing but here we are introducing a special rule just when the wretched bar follows certain named productions. That seems so out of place in 1.1.4 right at the beginning of the RM when we have absolutely no idea what the productions are for. * the vertical bar smells of OR to me and there is no ORishness in this code * it is said that some mathematics uses the vertical bar; however, we are not writing mathematics but doing programming. * the vertical bar is just too weak a symbol. We need something bigger and bolder to separate the two parts of the quantified expression * Spark has used the combination => for this purpose for many years and there seems no reason why we should not be consistent with existing usage Note that the !discussion in the AI says Instead of a vertical bar, we could use a colon or a right arrow to separate the iterator from the condition. The proposed syntax is more common in mathematics but the vertical bar has already other uses in the Ada syntax. This seems to me to be arguing for not using the vertical bar and one expects this to be followed by another sentence coming to that conclusion. But it just stops. Another point is that we need to take care to make it clear what things are grouped together. The syntax in Spark puts the predicate in parentheses and that seems to me to be a good thing to do. So the above examples would look like for all I in A'First..T'Pred(A'Last) => (A(I) <= A(T'Succ(I))) pragma Assert(for some X in 2 .. N/2 => (N mod X = 0)) This AI was sent back by WG9 last time in order to make "some" a proper reserved word. Perhaps we could give it another rethink. **************************************************************** From: Tucker Taft Sent: Wednesday, September 15, 2010 10:33 AM I have no problem with the "|" but I understand that others do. Taking our cue from existing SPARK syntax seems reasonable and using "=>" would be fine. I don't see the need for parenthesizing the predicate, since it can certainly be done when it helps readability, but given that the whole construct is parenthesized, it will be redundant in many cases. **************************************************************** From: Bob Duff Sent: Wednesday, September 15, 2010 10:50 AM > This AI was sent back by WG9 last time in order to make "some" a > proper reserved word. Perhaps we could give it another rethink. I can live with "=>" instead of "|". I think requiring parens around the predicate would be annoying if the predicate is a primary: Assert(for all I in A'Range => Is_Good(A(I))); Assert(for all I in A'Range => (Is_Good(A(I)))); **************************************************************** From: Edmond Schonberg Sent: Wednesday, September 15, 2010 12:34 PM The vertical bar is indeed standard mathematical usage, but I have no problem with other choices if there is such strong objection (and blood pressure issues). The most compelling argument is consistency with SPARK at this point, so I'll be happy to go with => . I looked at what Z does, but they live in their own beyond-ASCII world, including proper quantifier symbols. **************************************************************** From: Jean-Pierre Rosen Sent: Wednesday, September 15, 2010 12:44 PM > The vertical bar is indeed standard mathematical usage, but I have no > problem with other choices if there is such strong objection (and > blood pressure issues). Of course, there are three of us who could argue for compatibility with SETL ;-), but I have no more serious objection to => **************************************************************** From: Robert Dewar Sent: Wednesday, September 15, 2010 12:55 PM I prefer the vertical bar (mathematics and setl familiarty I think), but I agree that SPARK compatibility is a strong argment and can live with => **************************************************************** From: John Barnes Sent: Wednesday, September 15, 2010 2:56 PM My blood pressure is now quite reduced with the thought that => would be acceptable. Although I would prefer the parens, I am happy to forego them. Spark does use a lot of parens - possibly Pascal influence. (That is the language Pascal and not M Leroy.) **************************************************************** From: Robert Dewar Sent: Wednesday, September 15, 2010 3:22 PM I definitely do NOT like the junk extra parens **************************************************************** From: Randy Brukardt Sent (privately): Saturday, September 15, 2010 12:53 AM 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 > 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 > inconsistent. Given that "iterator_specification" is defined by an AI that is very much still under construction, I have no idea what could or should be written in the Dynamic Semantics. I surely don't want to repeat complex rules here. Therefore, I suggest that we table this AI until AI05-0139-2 is done. --- > 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. Indeed, using "=>" would be very confusing with the aggregate syntax of (for I in Positive => Func(I)) or (for I in Arr_Type'Range => new D(I)) which has been repeatedly proposed to allow initializations based on the array index (including today on comp.lang.ada, which is why I thought of it). But the SPARK argument does seems to be compelling. **************************************************************** From: Christoph Grein Sent: Thursday, November 18, 2010 1:15 AM !topic AI05-0147-1 AI05-0176-1 !reference Ada 2005 RM-4.5.7(5.3), RM-4.5.9(4/3) !from Author Grein 2010-11-18 !keywords while loop conditional_expression quantified_expression !discussion Quote RM-4.5.9(4/3): "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." Suppose P (X) is some boolean expression. Then: while (for all X in A'Range => P (X)) loop -- ugly, but understandable while (for some X in A'Range => P (X)) loop -- what should this mean? Also conditional expressions look bad in this context. Is this really the intent? **************************************************************** From: Edmond Schonberg Sent: Thursday, November 18, 2010 8:43 AM > while (for some X in A'Range => P (X)) loop -- what should this mean? Exactly what it says: iterate as long as there is at least one element in the range of A that satisfies the predicate. The existentially quantified expression is a boolean condition, evaluated each time through the loop. **************************************************************** From: Cyrille Comar Sent: Thursday, November 18, 2010 9:21 AM > Suppose P (X) is some boolean expression. Then: > > while (for all X in A'Range => P (X)) loop -- ugly, but > understandable the "while" loop continues as long as P(A'First) .. P(A'Last) are all true and stops as soon as one of those is false > while (for some X in A'Range => P (X)) loop -- what should this mean? the "while" loop continues as long as there is at least one in P(A'First) .. P(A'Last) that is true and stops when they are all false. > Also conditional expressions look bad in this context. Is this really > the intent? if this was what you intended to express, it looks to me that it is a pretty good way to express it. The "old" way of expressing the same thing is much more verbose and not particularly readable: while (All_Are_True (A, P'Access)) loop ... while (One_Is_True (A, P'Access)) loop ... where function All_Are_True (A : Type_of_A; P : access function (X : type_of_X) return Boolean) is begin for I in A'Range loop if not P.all (I) then return False; end if; end loop; return True; end All_Are_True; etc... ****************************************************************