!standard 2.9(2/2) 10-02-22 AI05-0176-1/03
!standard 3.3(19)
!standard 4.4(7)
!standard 4.5.9(0)
!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 quantified expressions over a finite domain.
!problem
It is very common in formal development to define a predicate over a collection
to express the fact that all elements of the collection satisfy a given property
or that at least one element of the collection satisfies it. (This is of course
borrowed from the language of set theory and fornal logic). For example, the
fact that an array A is sorted can be expressed by stating that for all values
of an index I in the range from A'First to A'Last - 1 inclusive, the property
A(I) <= A (I+1) obtains. Mathematical usage is to write, e.g. forall X | P (X),
to indicate that all elemnts X satisfy the property P (X).
When using such notation, the context is supposed to indicate the universe in
which the elements X are to be found. This is of course not usable in a
programming language that is meant to be executable, and the syntax must
indicate the domain of definition of the element (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:
boolean expressions that verify whether all (resp. al least one) element in a
collection (array or container) satisfies a given predicate. Introduce a
non-reserved keyword: "some" to support this feature.
Quantified expressions have the following syntax:
( for quantifier loop_parameter_specification | Boolean_Expression )
The loop_parameter_specification is the one proposed in AI05-0139-2 for
iterators. It includes default iterations over discrete ranges and over
containers, as well as user-defined iterations over such.
!wording
Add 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.9 Quantified expressions
quantified_expression ::=
(quantifier defining_identifier in domain | predicate)
quantifier ::= for all | exists
domain ::= discrete_subtype_definition | expression
predicate ::= boolean_expression
Name Resolution Rules
The expected type of a quantified expression is the predefined type Boolean.
The predicate in a quantified_expression is expected to be of any boolean type.
Dynamic Semantics
The evaluation of a quantified expression evaluates the predicate for each
value of the loop_parameter. These values are examined in the
order specified by the loop_parameter_specification.
The value of the quantified expression is determined as follows:
* If the quantifier is "all" the expression is True if the evaluation of the
predicate yields True for each value denoted by the loop_parameter. It is
False otherwise. Evaluation of the quantified expression stops when all values
of the domain have been examined, or when the predicate yields False for a
given value. Any exception raised by evaluation of the predicate is
propagated.
AARM note: the expression is True if the domain contains no values.
* If the quantifier is "some" the expression is True is the evaluation of the
predicate yields True for some value of the loop_parameter. It is False
otherwise. Evaluation of the expression stops when all values of the domain
have been examined, or when the predicate yields True for a given value. Any
exception raised by evaluation of the predicate is propagated.
AARM note: the expression is False if the domain contains no values.
Examples
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)))
The assertion that a positive number is composite can be written:
(for some X in 2 .. N / 2 | N mod X /= 0)
!discussion
Instead of a vertical bar, we could use a colon or a right arrow to separate the
iterator from the condition. The proposed notation is more common in mathematics
but the vertical bar has already other uses in Ada syntax.
The order of evaluation is fixed by the iterator used in the
loop_parameter_specification, so there is a strong assumption of sequentiality.
Not clear how to indicate that a quantified expression can be evaluated in
parallel, given that we have no mechanism to parallelize loops either.
!example
(See Wording.)
--!corrigendum 4.5.9(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 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: Robert Dewar
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?
****************************************************************