Unformatted version of **ai05s/ai05-0176-1.txt version 1.2**

Other versions for file**ai05s/ai05-0176-1.txt**

Other versions for file

!standard 4.5.1 09-10-28 AI05-0176-1/01

!class Amendment 09-10-28

!status work item 09-10-28

!status received 09-10-28

!status received

!priority Low

!difficulty Easy

!subject Quantified expressions

!class Amendment 09-10-28

!status work item 09-10-28

!status received 09-10-28

!status received

!priority Low

!difficulty Easy

!subject Quantified expressions

!summary

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

!problem

It is very common in formal developement to define a predicate over a collection
to express the fact that all elements of the collection satisfy a given
property. (This is of course borrowed from the language of set theory and fornal
logic). For example, the fact that an array A is sorted can be expressed by
stating that for all values of an index I in the range from A'First to A'Last -
1 inclusive, the property A(I) <= A (I+1) obtains. Mathematical usage is to
write, e.g. forall X | P (X), to indicate that all elemnts X satisfy the
property P (X). When using such notation, the context is supposed to indicate
the universe in which the elements X are to be found. This is of course not
usable in a programming language that is meant to be executable, and the syntax
must indicate the domain of definition of the element. The common notation is:
forall X in domain | P (X).

The domain can be a range, or an expression that designates a container. The
first is typically used when the collection is an array, and the index
(the bound variable in the expression) is used to denote an element of the
collection in the condition. For collections with no built-in ordering, the
bound variable denotes directly an element of the collection:

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

Directory may be one of the predefined containers, or an array.

Such expressions will prove very useful in pre/post conditions and invariants.

!proposal

Quantified expressions have the following syntax:

( for all defining_identifier in Domain | Boolean_Expression )

Domain => Discrete_Range | Expression

!wording

<tbd>

!discussion

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

When quantifying over an array, the syntax provides the index, i.e. a cursor
over the array. There is no obvious domain over which to define a cursor in the
case of a container, so the notation (for all X in C | P (X)) is natural.
However, for the case of Maps, it would be attractive to have a form that
binds both a key and the corresponding element in the container. This suggests
introducing an attribute 'Domain (we already have 'Range) so we could write

(for all Key in M'Domain ( Find (M, Key) > 7)

Given that a mapping has a domain and a range, this suggests generalizing both
of these attributes to be used in quantified expressions and in loops, but
this is probably too big a change at this time.

!example

** TBD **

--!corrigendum 4.5.1(0)

!ACATS test

Add an ACATS C-Test to test the syntax.

!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 you 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 the basics). 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 imperative 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 <identifier> <parameter and result profile> renames <expression> 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. ****************************************************************

Questions? Ask the ACAA Technical Agent