Version 1.3 of ai05s/ai05-0177-1.txt

From: Bob Duff
Date: Sunday, March 15, 2009  9:37 AM

[Editor's note: This forked off of a discussion about conditional expressions,
found in AI05-0147-1.]

> I must say I still like to abstract complex conditionals into
> predicate functions.

Agreed.  Which means that if you want to use a conditional in a precondition,
you (sometimes) want to put the BODY of a boolean function in a package SPEC, so
it is not hidden from the compiler!

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

From: Randy Brukardt
Date: Monday, March 16, 2009  2:06 PM

> I must say I still like to abstract complex conditionals into
> predicate functions. People manage to write frighteningly complex
> conditions without this feature, and I am afraid that this will get
> worse with the addition of this feature. Still possible misuse is not
> a reason for prohibition!

I tend to agree. I actually thought about making such predicate function easier
by defining expression renamings, but I didn't think I could sell it as
important enough to bother with. The idea was something like:

   function Is_Interesting (N : in Natural) return Boolean renames (N > 10);

Of course, the expression could be as complex as needed. If this is defined in a
specification (or other place where the renames is "visible"), I could even
imagine rules allowing this to be treated as a static expression. This would be
nice because it would not be a barrier to static analysis like a normal function
body that may not be available to the analyzer.

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

From: Randy Brukardt
Date: Monday, March 16, 2009  2:11 PM

> > I must say I still like to abstract complex conditionals into
> > predicate functions.
>
> Agreed.  Which means that if you want to use a conditional in a
> precondition, you (sometimes) want to put the BODY of a boolean
> function in a package SPEC, so it is not hidden from the compiler!

All you need is Randy's handy dandy expression renames (see my reply to Robert).

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

From: Robert Dewar
Date: 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.
[Editor's note: The message being replied to here is in AI05-0176-1.]

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: Randy Brukardt
Date: Monday, March 16, 2009  5:01 PM

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

That's surely true, but to be fair, the idea of renaming of expressions is mine
and mine alone. I suggested it in passing at the Tallahassee meeting and
received approximately 0% interest. Perhaps I didn't have the justification
strong enough...

> I find the bodies-in-spec issue to be a significant one!

So do I. One alternative would be a modifier that specifies (in some way -
keyword, pragma) functions that have no side-effects other than through their
interfaces. Such functions can be used in static symbolic analysis based on
their parameters; that's not as good as being able to see the entire body, but
surely better than being able to assume nothing about the behavior of the
function.

Since you and others have expressed dislike of that idea, I'll spend my energies
on other ideas, possibly including renaming of expressions.

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

From: Gary Dismukes
Date: Monday, March 16, 2009  5:21 PM

> That's surely true, but to be fair, the idea of renaming of
> expressions is mine and mine alone. I suggested it in passing at the
> Tallahassee meeting and received approximately 0% interest. Perhaps I
> didn't have the justification strong enough...

It sounds like a reasonable sort of feature to me.

In fact, it's a little odd that in Ada one can rename function calls, including
uses of predefined operators:

   C : Boolean renames "and"(A, B);

but you can't rename the infix form:

     C : Boolean renames (A and B);  -- ERROR

Seems like a short step to extend renamings to allow expressions generally (even
though of course these couldn't be classified as object renamings in the general
case, they'd have to be a separate category).

> > I find the bodies-in-spec issue to be a significant one!
>
> So do I. One alternative would be a modifier that specifies (in some
> way - keyword, pragma) functions that have no side-effects other than
> through their interfaces. Such functions can be used in static
> symbolic analysis based on their parameters; that's not as good as
> being able to see the entire body, but surely better than being able
> to assume nothing about the behavior of the function.
>
> Since you and others have expressed dislike of that idea, I'll spend
> my energies on other ideas, possibly including renaming of expressions.

Yes, I would rather have you pursue expression renamings. :-)

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

From: Tucker Taft
Date: Monday, March 16, 2009  5:25 PM

I don't personally find bodies-in-the-spec a big issue.

There will always be times when you want to define a predicate which is too
complex to be used in the spec.  Furthermore, it is inappropriate because it
depends on private fields, etc.  It is one thing to specify the precondition in
the spec, which is important.  However, it is not necessary for the full
semantics of the precondition to be in the spec, since any static analysis tool
of any value to a language like Ada will need to be able to look in bodies.

I suppose if we were queasy about having the tool look in all bodies, we could
have a pragma analogous to Inline that indicates that a particular subprogram is
to be effectively "inlined" for the purpose of static analysis.

I really believe that at some point we want to stop adding special syntax, and
fall back on using the programming language, which is already more than Turing
complete.  Subprograms are the key way we do that, and trying to pull the full
power of the programming language into an expression language seems misguided
for Ada, particularly given the importance of private types.

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

From: Tucker Taft
Date: Monday, March 16, 2009  5:33 PM

> I don't personally find bodies-in-the-spec a big issue.

Let me clarify.  I don't want to see bodies in the spec.  What I mean is that I
don't mind having preconditions that include calls on functions where the
analyzer needs to look at their body to know what they do.  I think it is
inevitable. We have been talking about using containers in these quantified
expressions.  The semantics of containers certainly isn't going to be fully
visible in the spec!

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

From: Bob Duff
Date: Monday, March 16, 2009  5:20 PM

> So I see these quantified expressions as significantly lower priority
> than conditional expressions.

I agree, but I'll repeat my comment: I want to have the option of putting
function bodies in package specs.

Subroutines with parameters were invented a long time ago, and they are really
the most wonderful abstraction mechanism.  It's a Bad Thing anytime you lose
something by wrapping some code up in a subroutine.

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

From: Randy Brukardt
Date: Monday, March 16, 2009  5:51 PM

...
> I don't personally find bodies-in-the-spec a big issue.
>
> There will always be times when you want to define a predicate which
> is too complex to be used in the spec.
> Furthermore, it is inappropriate because it depends on private fields,
> etc.

I was presuming that such an expression renames could be used as a
renames-as-body in the private part, thus getting access to the private
components without making them directly visible to clients, but still making
them available to analyzers. Seems like the best of all worlds to me.

> It is one thing to specify the
> precondition in the spec, which is important.  However, it is not
> necessary for the full semantics of the precondition to be in the
> spec, since any static analysis tool of any value to a language like
> Ada will need to be able to look in bodies.

Here I disagree. I think the most useful static analysis is going to be that
which is part of a compiler. That means that bodies aren't necessarily going to
be available to the analyzer, only specifications. (This also allows analyzers
to do good work on partial programs.)

Indeed, I just (literally an hour ago) read an article on embedded.com that
makes the same point. http://www.embedded.com/210601784?cid=NL_embedded (it's an
older article that they linked for some reason today). I also recall reading an
article where Robert Dewar made some similar suggestion.

I realize that you know 10 times more about static analysis than I do, so I
could be all wet on this.

> I suppose if we were queasy about having the tool look in all bodies,
> we could have a pragma analogous to Inline that indicates that a
> particular subprogram is to be effectively "inlined" for the purpose
> of static analysis.

Inline still requires the body to exist. I think we really need to be able to
reason about functions whose bodies don't yet exist. (But, I know, I'm still a
minority of one on that point.)

Besides, I'm opposed to specifying inlining/allowing dependencies because of
inlining. I think that the compiler should be deciding such stuff, it has a far
better idea of the trade-offs than any programmer can. The programmer should
simply set a time/space trade-off for a program and get out of the way. Pragma
Inline and similar features are a hack used when compilers didn't have enough
CPU/memory to do these things automatically -- but that time is long gone.

> I really believe that at some point we want to stop adding special
> syntax, and fall back on using the programming language, which is
> already more than Turing complete.
> Subprograms are the key way we do that, and trying to pull the full
> power of the programming language into an expression language seems
> misguided for Ada, particularly given the importance of private types.

I don't disagree with this sentiment (a simple "for all" expression didn't
bother me too much, but the latest stuff I've seen seems over the top). But I do
worry about restricting the ability to do analysis at compile-time.

One reason that I proposed expression renaming is that I don't want the full
complexity of a subprogram body in package specifications. But since expressions
are already there, I don't see any problem with putting more of them there.
Indeed, one could imagine using this facility to define the "identity functions"
that we talked about in Tallahassee (seems better than a dedicated feature).

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

From: Bob Duff
Date: Monday, March 16, 2009  5:34 PM

> > Agreed.  Which means that if you want to use a conditional in a
> > precondition, you (sometimes) want to put the BODY of a boolean
> > function in a package SPEC, so it is not hidden from the compiler!
>
> All you need is Randy's handy dandy expression renames (see my reply
> to Robert).

Randy's handy dandy expression renames might be a nice idea.
But what if I want the thing to have a local variable or something?
Seems like it might end up being one of those frustrating features that gives
you ALMOST what you want, but not quite.  Better than nothing? Not sure.

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

From: Tucker Taft
Date: Monday, March 16, 2009  7:01 PM

> Agreed.  Which means that if you want to use a conditional in a
> precondition, you (sometimes) want to put the BODY of a boolean
> function in a package SPEC, so it is not hidden from the compiler!

I don't understand this.  Package bodies aren't hidden from the compiler.  The
compiler can look in a package body any time it wants, and it is expected to do
so for inlines and frequently generics.  Of course that may mean more
recompilation if the body changes, but we accept that for inlines and generics.

Separating spec and body is fundamental in Ada, and it is not so much for the
compiler as for the humans.  If anything I would think we would want to go the
other way, and be taking things out of the specs, such as the completion of a
private type.

The only part of a precondition that needs to be in the spec is the
"specification" of the precondition. It's full semantics can and often should be
postponed to a package body, as the full semantics depend on information that is
intentionally hidden in the package body.

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

From: Robert Dewar
Date: Monday, March 16, 2009  7:14 PM

> I don't understand this.  Package bodies aren't hidden from the
> compiler.  The compiler can look in a package body any time it wants,
> and it is expected to do so for inlines and frequently generics.  Of
> course that may mean more recompilation if the body changes, but we
> accept that for inlines and generics.

But you should be able to verify a client with only the package spec in view (it
makes sense to verify a client even before the body exists).

> Separating spec and body is fundamental in Ada, and it is not so much
> for the compiler as for the humans.  If anything I would think we
> would want to go the other way, and be taking things out of the specs,
> such as the completion of a private type.

But precoonditions are part of the spec

> The only part of a precondition that needs to be in the spec is the
> "specification" of the precondition.
> It's full semantics can and often should be postponed to a package
> body, as the full semantics depend on information that is
> intentionally hidden in the package body.

I disagree, generally the full semantics of the precondition should be there in
the spec, especially if you want to view them as formal mathematical properties
that go into a theorem prover, or a sophisticated semantic analyzer.

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

From: Randy Brukardt
Date: Monday, March 16, 2009  7:17 PM

...
> I don't understand this.  Package bodies aren't hidden from the
> compiler.  The compiler can look in a package body any time it wants,
> and it is expected to do so for inlines and frequently generics.  Of
> course that may mean more recompilation if the body changes, but we
> accept that for inlines and generics.

Well, maybe you do, but I don't. Inline and generic body dependencies are both
optional, and Janus/Ada has never had and most likely never will have any sort
of body dependency. (This was the original reason that we implemented generics
as code shared, which should make it clear to you the lengths that I am willing
to go to preserve this point!) Inlining is better implemented at link time,
anyway, and shouldn't require any human intervention in the first place.

Any feature that were to require a body dependency would be strenuously opposed
by me!

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

From: Robert Dewar
Date: Monday, March 16, 2009  7:18 PM

> So do I. One alternative would be a modifier that specifies (in some
> way - keyword, pragma) functions that have no side-effects other than
> through their interfaces. Such functions can be used in static
> symbolic analysis based on their parameters; that's not as good as
> being able to see the entire body, but surely better than being able
> to assume nothing about the behavior of the function.

Just not enough, if I see

     procedure A (B, C : Integer);
     pragma Precondition (P (B, C));

there are two cases

a) P is a complex computational procedure, beyond the reach of a theorem prover,
   or a semantic analyzer. Fine, in this case it is just a run-time check that
   can go in the spec. There is no issue of formally verifying that a call to P
   meets this precondition.

b) P is a predicate that is statically understandable, it is a conditional
   expression, or series of conditional expressions in some canonical form,
   possibly including quantifiers. In this case you want the "body" of P visible
   in the spec.

Note that in case a), it is of no interest at all to know that P is pure.

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

From: Randy Brukardt
Date: Monday, March 16, 2009  7:48 PM

Not quite true (although I agree that seeing the body is better). If the static
analyzer already knows the result of P (B, C) [perhaps because it is the
postcondition of a previous call], then if P has no side-effects, the analyzer
can use the previous result in this precondition and not further evaluate it.
That's a fairly likely case. And it is not something it can do otherwise
(assuming no side-effects is not something that a static analyzer should do,
especially if it is part of a compiler, as erroneousness could result from a bad
assumption -- surely do not want to be able to introduce erroneousness into a
program that otherwise doesn't have it, and especially as part of something that
is supposed improve correctness).

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

From: Stephen Michell
Date: Monday, March 16, 2009  8:03 PM

It is even simpler than that. The postconditions on pure functions can be
assumed after the point of the call. I am assuming that we have the notion that
pre(spec)->(pre(body) and post(body)->post(spec). One can safely mark the
condition as TRUE, pending analysis of the body. Body analysis will let us mark
the condition TRUE with no reservations, or mark if false later if the
postcondition analysis fails.

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

From: Tucker Taft
Date: Monday, March 16, 2009  8:09 PM

Well I suppose it should be refreshing for me not to be the one with the
wild-eyed over-the-top ideas for enhancing the language...  ;-) ;-) ;-)

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

From: Randy Brukardt
Date: Monday, March 16, 2009  7:20 PM

> But you should be able to verify a client with only the package spec
> in view (it makes sense to verify a client even before the body
> exists).

Darn right. Tucker seems to have a model where analysis is only done by a
separate tool after the entire program already exists. I think this is far too
late: we need to detect errors as early as possible in the development cycle
(preferably the first time we run a tool on the code).

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

From: Randy Brukardt
Date: Monday, March 16, 2009  7:37 PM

> Randy's handy dandy expression renames might be a nice idea.
> But what if I want the thing to have a local variable or something?
> Seems like it might end up being one of those frustrating features
> that gives you ALMOST what you want, but not quite.
> Better than nothing?
> Not sure.

Well, putting a full body in a specification is certain to bring up all kinds of
*interesting* freezing issues. We saw that for the various proposals to allow
early instantiations, and I don't think we particularly want to do there. OTOH,
we already have expressions in specifications, so both the language semantics
and compilers presumably can handle them. Indeed, it ought to be able to handle
them without freezing (they could be treated like default expressions), which
would *add* some capabilities that would currently be hard to write.

Also, these sorts of functions could be (ought to be?) automatically inlined;
the more complex stuff that you are allowed to write, the more likely it is that
you would run into some reason why inlining would be difficult.

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

From: Bob Duff
Date: Monday, March 16, 2009  8:04 PM

> I don't understand this.  Package bodies aren't hidden from the
> compiler.  The compiler can look in a package body any time it wants,
> and it is expected to do so for inlines and frequently generics.  Of
> course that may mean more recompilation if the body changes, but we
> accept that for inlines and generics.

Compilers can look at bodies any time they want for code-gen stuff.
But the Ada language is designed so that legality issues are always determinable
from specs (visible parts, actually).

Proving assertions statically is just an extension of legality checking, and
should (ideally) likewise depend only on visible parts of imported packages.

> Separating spec and body is fundamental in Ada, and it is not so much
> for the compiler as for the humans.  If anything I would think we
> would want to go the other way, and be taking things out of the specs,
> such as the completion of a private type.

Agreed.

> The only part of a precondition that needs to be in the spec is the
> "specification" of the precondition.
> It's full semantics can and often should be postponed to a package
> body, as the full semantics depend on information that is
> intentionally hidden in the package body.

Yes, that's quite often true.  But not always.

If you have a precondition that looks at private stuff, then I agree -- it
should call a function whose body is in the package body.

But sometimes a precondition involves visible stuff, and in that case it should
be visible, and it's annoying that giving it a name as a function causes it to
be invisible.

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

From: Robert Dewar
Date: Monday, March 16, 2009  8:08 PM

> Well, maybe you do, but I don't. Inline and generics are both
> optional, and Janus/Ada has never had and most likely never will have
> any sort of body dependency. (This was the original reason that we
> implemented generics as code shared, which should make it clear to you
> the lengths that I am willing to go to preserve this point!) Inlining
> is better implemented at link time, anyway, and shouldn't require any human intervention in the first place.
>
> Any feature that were to require a body dependency would be
> strenuously opposed by me!

I don't regard this as a valid argument at this stage, and I think there are
better arguments in any case. I think we have already paid too high a price in
determining to maintain the (to me very dubious) possibility of fully shared
generics.

As for inlining being better at link time, this to me is technically quite
wrong, one of the major advantages of inlining is to activate the full set of
flow-based optimizations to the inlined code. That cannot be done at link time.

But in any case, I think the implementation based arguments on this issue are
not the strong ones. The strong argument is conceptual. Preconditions are part
of the spec, so they should be in the spec. End of story as far as I am
concerned.

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

From: Robert Dewar
Date: Monday, March 16, 2009  8:13 PM

> If you have a precondition that looks at private stuff, then I agree
> -- it should call a function whose body is in the package body.

To me such preconditions are really part of the body anyway

> But sometimes a precondition involves visible stuff, and in that case
> it should be visible, and it's annoying that giving it a name as a
> function causes it to be invisible.

I agree with this

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

From: Robert Dewar
Date: Monday, March 16, 2009  8:15 PM

> Well I suppose it should be refreshing for me not to be the one with
> the wild-eyed over-the-top ideas for enhancing the language...  ;-)
> ;-) ;-)

:-)

Yes, that maniac Dewar is always wanting to add over-complex features :-)

What can I say? Every now and then, I get distracted into thinking Ada is a high
level language :-)

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

From: Randy Brukardt
Date: Monday, March 16, 2009  8:27 PM

...
> As for inlining being better at link time, this to me is technically
> quite wrong, one of the major advantages of inlining is to activate
> the full set of flow-based optimizations to the inlined code. That
> cannot be done at link time.

Bull. The design that I have does full optimization at link-time: simply by
linking and inlining the intermediate code, then optimizing and code generating.
Code generators are fast enough that there isn't much need to do that early
anymore.

(Of course, I'm talking only about the Ada portion of the program; you might
need an extra linking step to link in foreign language code.)

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

From: Robert Dewar
Date: Monday, March 16, 2009  8:36 PM

Yes, well that's easy to design in your head! But nonsense in most practical
environments, or at the least a research effort. Optimization algorithms are not
linear with program size, or even quadratic, and it is simply not the case that
highly optimizing code generators are fast enough to apply to large scale
programs, without a lot of work.

We can't let ourselves be influenced by unrealized plans!

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

From: Randy Brukardt
Date: Monday, March 16, 2009  9:15 PM

The non quadratic nature of optimization is something that I am acutely aware
of. Indeed, our early optimizer efforts effectively locked up the processors of
the late 1980's. That's why our optimizer has a serious set of time-limiters in
it; we already do full subprogram optimization on most subprograms and I don't
think that we would want to do inter-procedural optimizations anyway (other than
inlining, dead code elimination, and partial evaluation, none of which need to
be particularly expensive to implement).

Thus I know our optimizer and code generator performance would be essentially
linear from current behavior, since there is nothing that we would do that would
require working on larger chunks of code. (We'd use the same limiting code for
the same reasons.) Multicore machines offer the promise of actually doing better
still (because we could optimize multiple subprograms at a time), although that
is obviously more work.

There is an advantage to being a bit behind state-of-the-art in code generator
technology! :-)

> We can't let ourselves be influenced by unrealized plans!

Fair enough (although I've read several articles about such compilers in the
last year or so). It's unfortunate that I can't find the 1-2 man months it would
take to put this together (since it is just rearranging the pieces of our
compiler). I'd like to know if this scheme really works as well in practice as
it does on paper.

Anyway, I would not like adding new body dependencies, period.

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

From: Edmond Schonberg
Date: Monday, March 16, 2009  8:42 PM

> The only part of a precondition that needs to be in the spec is the
> "specification" of the precondition.
> It's full semantics can and often should be postponed to a package
> body, as the full semantics depend on information that is
> intentionally hidden in the package body.

Mild objection:  the client of the package should be able to know what the
precondition actually means: a contract that says " we'll reject any input that
doesn't glorp"  is not very useful if you don't know what it means to glorp.
THis is why a rich language of expressions for preconditions seems preferable to
me than one where the body of the predicates is actually off-line. I understand
that this may be needed in some cases, but my preference would be for
preconditions that can be written and read up-front.

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

From: Robert Dewar
Date: Monday, March 16, 2009  8:52 PM

I am generally sympathetic to this approach, but am afraid of large conditional
expressions without any kind of abstraction.

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

From: Randy Brukardt
Date: Monday, March 16, 2009  9:16 PM

I agree. Large Boolean expressions are notoriously hard to read and debug.

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

From: Edmond Schonberg
Date: Monday, March 16, 2009  9:26 PM

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
Date: 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: Randy Brukardt
Date: Tuesday, March 17, 2009  12:07 AM

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

That's fine if the compiler knows that Sorted is Strict (or Pure, if you prefer
to overload that term). But how it can know that without a pragma/keyword of
some sort (or seeing the body) is beyond me. (Very few of these abstractions are
going to be Pure packages, after all).

If Sorted is defined:
    function Sorted (A : in <Whatever>) return Boolean is
    begin
        if Random < 0.2 then return False;
        else return True;
        end if;
    end Sorted;
any symbolic manipulation that is done is simply going to be wrong, because the
result of one call to this function is not going to be related to another. (A
more realistic example would depend on a global data structure as well as the
input parameter. If the global data changes, so might the result of the function
call.)

Without any sort of requirement or way to tell if these functions are strict, I
don't see how you can do any symbolic manipulation. (We haven't even *suggested*
to users that their functions shouldn't have side-effects in these. And I don't
see how we could in any valuable way.)

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

I tend to agree, in that is the way I was expecting it to work in practice.
For instance, in Claw we'd surely want Is_Valid preconditions and postconditions
on the various routines.

But I don't see any justification for assuming that the values of multiple calls
to a function are the same. And without that, you can't do anything at all.

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

From: Tucker Taft
Date: Tuesday, March 17, 2009  12:42 AM

It seems you are agreeing that programmers will be defining these "helper"
functions, so does that mean you agree that we probably don't need to work too
hard to support bodies in specs, quantified expressions, etc?

I agree the "analyzer" will need some way to know what variables these helper
functions read other than their explicit parameters.  Perhaps we need to have
"Global_In" and "Global_Out" annotations as well as Pre and Post, where any
function used in a precondition, that lacks a "Global_In" annotation, is
presumed to read no variables other than its parameters.  This could be checked
when processing the body of such a function.

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

From: Randy Brukardt
Date: Tuesday, March 17, 2009  12:42 AM

> It seems you are agreeing that programmers will be defining these
> "helper" functions, so does that mean you agree that we probably don't
> need to work too hard to support bodies in specs, quantified
> expressions, etc?

Well, I think renaming of expressions would be allow increasing abstraction
without impacting performance, freezing, or analyzability. What's not to like?
:-) You could even hide the actual expressions in the private part and thus
write simple predicates without sacrificing hiding.

I don't think including full bodies in specifications would work, because of
freezing issues. That's irrespective of whether or not it is a good idea.

Quantified expressions seem like too specialized a need to me, but on this one I
will defer to people who know more about this than me.

> I agree the "analyzer" will need some way to know what variables these
> helper functions read other than their explicit parameters.  Perhaps
> we need to have "Global_In"
> and "Global_Out" annotations as well as Pre and Post, where any
> function used in a precondition, that lacks a "Global_In"
> annotation, is presumed to read no variables other than its
> parameters.  This could be checked when processing the body of such a
> function.

Humm. Ada allows *anything* currently, so I don't think the absense of
specification can mean "no side effects". Remember, I want to be able to make
some of this analysis at compile-time, and surely we want to support "partial"
preconditions, postconditions, and so on. Wasn't it you that said that you could
use whatever information is provided? I don't think most applications are going
to want to specify every detail, but that isn't to say that stronger contracts
would be useless in such applications.

In any case, I would like to keep the special behavior of these guys to a
minimum. We already have special attributes only for use in postconditions, but
it doesn't seem that can be helped (because of efficiency concerns). I really
don't want to see more special gizmos.

Anyway, my point is that no specification ought to mean anything goes (as it
does now in existing functions); that means that there also would need to be a
specification of no side effects. Something like Global_In => null. Isn't
Global_In a list of names anyway? It surely isn't a Boolean expression! So it
can have some other syntax (would have to, in fact).

I would think that if Global_In is specified and it is wrong (that is, other
globals are referenced), the program should be rejected. This is a case where
wrong information is actively harmful; no information at all is better.

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

From: Randy Brukardt
Date: Thursday, March 19, 2009  12:01 AM

> Well, I think renaming of expressions would be allow increasing
> abstraction without impacting performance, freezing, or analyzability.
> What's not to like? :-) You could even hide the actual expressions in
> the private part and thus write simple predicates without sacrificing
> hiding.
>
> I don't think including full bodies in specifications would work,
> because of freezing issues. That's irrespective of whether or not it
> is a good idea.

In order to make it more possible for Tucker to know what he's rejecting ;-),
here is a more detailed explanation of what I had in mind for renaming of
expressions.

---

   renamed_expression ::=
      [overriding_indicator]
      function_specification renames (<*renamed_*expression>);

[Note: The parens are needed to clearly (?) separate renaming an expression as a
function from renaming some other function as a function. Perhaps it would be
better to use a keyword somewhere to make it crystal-clear.]

The expected type of the renamed_expression is that of the return subtype of the
function_specification.

Within the renamed_expression, the parameters of the function_specification are
visible. (This would work the same way as the parameters are visible within a
precondition.)

The dynamic semantics are the same as a function whose body contains nothing but
"return renamed_expression".

This renames could be used as a renames-as-body or as a renames-as-declaration.
(A renames-as-body could appear in the private part to complete a subprogram
declared in the visible part, as well as in the body.)

Freezing: The renamed expression would freeze as does a default expression. That
is, freezing would only be performed at the point of a call of the function,
with the expression essentially in-lined at that point. (Of course, if that call
is in the default expression, the freezing would be deferred again.)

Elaboration: I believe that freezing is enough for this construct to ensure that
the types of this construct are elaborated, so that no elaboration check would
ever need to be made on an call of one of these renames. However, the
renamed_expression could include a (separate) call that needed an elaboration
check; in that case the check would have to be made (somewhere - in the body if
not inlined, and at the point of the inlined call if inlined). It's not
completely clear to me if there is enough benefit to defining these specially in
terms of elaboration, although it always seems like a good idea to eliminate
run-time checks. Perhaps it would be enough to point this fact out in an AARM
note so that implementors are aware of this to take advantage of it. (Note that
this is only true if the compiler *knows* that a construct is a renamed
expression; if this completes a visible function in a package body, then the
elaboration would be "normal".)

Staticness: One could imagine these functions (when visible) to be used in
static expressions if the inlined expression would be static. I'm not certain
this is a good idea, but it would definitely allow abstracting expressions that
currently are written as a giant single expression because they need to be
static. That's something you cannot do now.

Finally, this construct could be allowed as a primitive subprogram of an
interface. If we did that, we would get the benefit of the identity function
idea without adding anything special specifically for that case. (If we wanted
to add the generic default for that case, then it gets a bit messier, but not a
huge amount.) We would have to somehow include the expression in the matching
rules in order to deal with the Steve Baird problem for diamond inheritance with
interfaces. I'm not quite sure this is worth it, but it does add to the things
that you cannot do now.

---

I know that Bob has already complained that you cannot declare a local variable
in such a renames. The problem with that of course is that it requires adding a
scope somewhere, so the semantics is more complex than a simple inline
substitution. I suspect that if we headed down that road we'd quickly reach a
roadblock because of freezing issues (similar to the ones we had for partial
generic instances). This is a case where 3/4s of a loaf that can be had easily
is worth more than a whole loaf that is a really hard to get to (that is, is a
definitional problem).

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

From: Bob Duff
Date: Thursday, April 29, 2010  7:32 PM

AI05-0177-1.TXT -- Renaming of expressions as functions (Also called "expression
functions".)

At today's subgroup phone meeting, everybody except me supported this feature.
I was asked to explain why, and I gave a rather incoherent explanation (I'm not
good at thinking on my feet).  Plus everybody interrupted with objections before
I was done.  So let me try to summarize my opinions, for the record.

I think there is definitely some value in exposing the implementations (i.e.
body) of small-ish subprograms to clients, to allow proof tools to see that
information.  I don't think that applies JUST to functions used in assertions
(e.g. preconditions).

"Exposing to clients" should mean "in the visible part".  Private parts and
bodies are supposed to be hidden from clients.  That's the Ada model.

Expression functions are a poor tool for achieving the "expose to clients" goal,
because they are restrictive.  Why can't they be procedures? (Tucker suggested a
solution to that.)  Why can't they have locally-declared constants?  I hate
these kinds of choices:  I can have the advantages of expression functions, or I
can have the advantages of local constants, but I can't have both at the same
time.  Why not?

It's fine with me if some tools (possibly optionally) look at private parts. But
if they do, they might as well look at bodies, too.  Conceptually, private part
and body are both part of the "implementation"; only the visible part is
"specification".  In fact, they might as well look at all type extensions of a
given root type.  That's what's needed to "expose the implementation" in all
cases.  So I don't see any advantage to expression functions, for tools that
wish to break privacy.

But a modular analysis of a client should look only at visible parts of whatever
it calls.

My final point here is that I think globals annotations are a more fruitful
endeavor.  As proposed, they're not ready to be standardized, but I think
implementations can experiment with them, and should give that experimentation
higher priority than expression functions.

Which leads to a more general point:  There are two extremes for standards:

    (1) Never standardize anything until it's been implemented and used
        successfully.

    (2) Standardize first, then implement and use.

Both have serious problems.  Ada tends toward (2).  I'm saying we should move
more in the direction of (1), at least in this case.

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

From: Randy Brukardt
Date: Thursday, April 29, 2010  10:33 PM

> At today's subgroup phone meeting, everybody except me supported this
> feature.  I was asked to explain why, and I gave a rather incoherent
> explanation (I'm not good at thinking on my feet).  Plus everybody
> interrupted with objections before I was done.  So let me try to
> summarize my opinions, for the record.

Sorry about the interruptions. I think you were pausing to gather your thoughts
long enough that we thought you were done talking.

...
> Expression functions are a poor tool for achieving the "expose to clients"
> goal, because they are restrictive.  Why can't they be procedures?
> (Tucker suggested a solution to that.)  Why can't they have
> locally-declared constants?  I hate these kinds of choices:
> I can have the advantages of expression functions, or I can have the
> advantages of local constants, but I can't have both at the same time.
> Why not?

I don't see any way to accomplish a significantly less restrictive vision.
Honestly, I don't see much point (beyond the easier inlining) to doing this for
anything other than predicates. For the sorts of functions that occur as
predicates, either they are trivial combinations of component values, or they
require some complex operations that have no advantage to being exposed anyway.

For instance, if you need a local variable and a loop to implement a predicate,
it's not very likely to be analyzable anyway. (At least not with the tools that
Ada 2012 is going to be providing - we don't have loop invariants and the like.)
So there is no huge loss to having to put it into a body.

The big win is for the tiny one-liner accessor functions: these might as well be
exposed to any tool that cares to look (and especially the compiler).

> It's fine with me if some tools (possibly optionally) look at private
> parts.
> But if they do, they might as well look at bodies, too.
> Conceptually, private part and body are both part of the
> "implementation"; only the visible part is "specification".
> In fact, they might as well look at all type extensions of a given
> root type.  That's what's needed to "expose the implementation" in all
> cases.  So I don't see any advantage to expression functions, for
> tools that wish to break privacy.
>
> But a modular analysis of a client should look only at visible parts
> of whatever it calls.

Ada allows children to have visibility on the private part, so it's not correct
to claim that no one should look there. Compilers look there all the time, and
the runtime correctness of a program *depends* on what is found there. And what
we're trying to analyze is the runtime correctness, isn't it??

In any case, I think the most important thing is to allow *compilers* to be able
to do these sorts of analyses, without having to depend on anything that they
don't naturally have. A compiler always has access to the private part of a
package, and rarely has access to a body other than the one being compiled.
Compilers usually don't pay much attention to privacy once they've gotten the
legality rules out of the way - I don't think our compiler does any analysis on
the code whatsoever until after the stage where privacy and the like is
respected. (And of course there are runtime considerations which require
ignoring privacy.)

Why do I think compilers are so important? It's not so much compilers as
whatever is the first tool run on the source code to remove errors. It should be
possible to find the maximum number of errors immediately after finishing
writing the code for a single unit, because that's when they're easiest to fix.
These days, the first tool run is almost always the compiler (at least to do
deep analysis - some IDEs do some syntactic checking). For that to work, no
other units other than direct dependencies (in particular, no bodies) need
exist.

The other, related issue for me is that compilers have to be able to eliminate
most of these contracts in the same way that we eliminate most range checks.
Like range checks, turning off contracts is like using seat belts until you
leave the garage - it's something you shouldn't do. The effort to do that can
naturally be used to also help the programmer see where their contracts are
iffy. Doing that is necessarily going to require looking under the hood, as all
optimization does to some extent or other.

> My final point here is that I think globals annotations are a more
> fruitful endeavor.  As proposed, they're not ready to be standardized,
> but I think implementations can experiment with them, and should give
> that experimentation higher priority than expression functions.

You are for some reason equating things that have very different orders of
magnitude. Expression functions probably will take a week or so of effort to
implement. Globals annotations are at least an order of magnitude more effort
(probably two orders). It doesn't make sense to say "don't spend a week
implementing an easy, useful feature because there is another feature that will
take 5 months to implement that might be more important". But the effort saved
will have no impact whatsoever on the results of the globals annotations.

I don't agree that the framework for globals annotations is not ready to be
standardized. The specific annotations that work best probably will require some
experimentation, but by not putting together a common framework populated with a
few important annotations which are obvious (specific items, everything in a
package, nothing at all), we're either going to end up with a tower-of-babble or
just as likely nothing at all. Even so, I understand why people feel this way
and am willing to go without. But what I will not stand for is having supposed
contracts with no way whatsoever for the compiler to analyze them if they're
written only in portable Ada. If we don't have one or the other, then I don't
want ANY new contracts in Ada. And I am going to fight that battle as long as I
can.

> Which leads to a more general point:  There are two extremes for
> standards:
>
>     (1) Never standardize anything until it's been implemented and used
>         successfully.
>
>     (2) Standardize first, then implement and use.
>
> Both have serious problems.  Ada tends toward (2).  I'm saying we
> should move more in the direction of (1), at least in this case.

I can buy that for globals annotations. Expression functions are completely
harmless even if you have them and follow your standard of visibility. They
don't do any good in that case, but they can always be treated as a normal
function. There's nothing really new here semantically (they work just like any
other function renames in terms of visibility, primitiveness, and the like). For
analysis purposes they are cost-free, since they will either be inlined or
called normally -- both of which an analyzer of any kind can already deal with.
Finally, since they cost almost nothing to implement (at least compared to any
other alternative), and even allow writing a few things that aren't currently
possible (because they defer freezing), it's hard to imagine how they are
harmful.

You are always telling us to not let "best" prevent us from adopting a solution
that is "good enough". Here is a solution that is good enough for 80% of
predicate functions, lets compilers at least have the information they need, has
very little cost since there is hardly anything new here (just a new combination
of existing pieces). You're saying that we can't have this solution because it
isn't "best". And *then* you go on and say we can't have the "best" solution
either because it needs more study. I can't imagine a more classic example of
letting "best" kill off "good enough"!!

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

From: Tucker Taft
Date: Friday, April 30, 2010  7:01 AM

I think I agree with Randy that this is a simple feature which will make a
significant pragmatic difference in the ability for compilers to do additional
compile-time analysis.  After all, in Ada 83, there was no real reason to have a
private part, except for pragmatic reasons associated with separate compilation.
The private part is exactly those things you need to provide the compiler when
compiling a *client* of an abstraction, to allow the compiler to generate
efficient code.  These expression functions seem to fit that purpose quite
exactly.

I don't particularly buy the notion that things in the private part shouldn't
affect whether some client code succeeds or fails at run-time; predicates are
clearly run-time semantics, not static semantics.  If a compiler chooses to emit
warnings about potential run-time failures at compile-time, that certainly is
its business, and it seems irrelevant whether it gleans that information from
the visible part, the private part, or the body, since clearly all three of
those places affect run-time semantics.

As an example of existing private-part information that might affect
compile-time warnings, consider whether a private type includes full default
initialization.  If the private type is implemented with a scalar type, then no
default initialization is provided.  If it is implemented with an access type,
then it is default initialized to null. If it is implemented using a composite
type, then how much of it is default initialized varies according to information
that is specified in the private part.

Clearly if you write:

    X : Priv_Type;
    Default_Value : constant Priv_Type := X;

it would make sense for the compiler to provide a compile-time warning if
Priv_Type is in fact implemented with a scalar type (or an array-of-scalar).

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

From: Robert Dewar
Date: Friday, April 30, 2010  5:08 PM

I completely  agree with Bob's position on this. I find restricting to an
expression to be hostile to good coding practice, since it results in having to
construct awkward complex expressions when simple sets of declarations and
statements would do better.

I also think these belong in the visible part, what on earth is the point of
having them in the private part? The private part is simply part of the
implementation separated off for convenience of the compiler (it should not even
be in the same file as the spec, and we plan to implement that separation in
GNAT some day).

Why is it convenient for the compiler to be able to see the body when the
programmer cannot? Well I guess for inlining, but we already have that
mechanism.

So in short I see no point whatever in renaming of expressions in the private
part, and if we allow it in the public part, we should just allow bodies in the
public part and be done with it.

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

From: Robert Dewar
Date: Friday, April 30, 2010  5:10 PM

> You are for some reason equating things that have very different
> orders of magnitude. Expression functions probably will take a week or
> so of effort to implement. Globals annotations are at least an order
> of magnitude more effort (probably two orders). It doesn't make sense
> to say "don't spend a week implementing an easy, useful feature
> because there is another feature that will take 5 months to implement
> that might be more important". But the effort saved will have no
> impact whatsoever on the results of the globals annotations.

By the way, in GNAT it is 5 mins work tyo allow bodies in the spec, because we
do anyway, we just have an arbitratry check to forbid it at the source level,
but we allow it in generated code (and all sorts of bodies are generated in the
spec).

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

From: Bob Duff
Date: Friday, April 30, 2010  5:19 PM

In fact all Ada compilers allow instance bodies in specs.

But that's a bit different, because nothing in the instance can refer to
anything in the outer spec (because the generic must have come from elsewhere).

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

From: Robert Dewar
Date: Friday, April 30, 2010  5:34 PM

The sort of thing we generate in GNAT is e.g. bodies of equality routines ...

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

From: Tucker Taft
Date: Friday, April 30, 2010  5:34 PM

I personally don't want to see bodies showing up in specs.  I think that really
confuses the model.

The idea behind limiting the capabilities is that these are intended for simple,
predicate-like things that need visibility on the full type, so clearly they
can't be in the visible part. They are in the private part simply so the
compiler can do a bit more compile-time analysis of preconditions,
postconditions, and subtype predicates without breaking separate compilation.

This seems to be a case where the "same" feature is of interest to two different
groups for almost diametrically opposed reasons, which in fact means the two
groups come up with opposite requirements for the feature, and hence it really
should be discussed as two different features:

   1) Arbitrary bodies anywhere in specs.

   2) Simple expression-level predicates in the private part.

I might note that we are limiting preconditions and postconditions and
assertions to expressions, so there is some precedent for having to live without
temporary variables, etc., when trying to express something relevant to static
analysis.  That's what these "expression-functions" really are.

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

From: Robert Dewar
Date: Friday, April 30, 2010  6:03 PM

OK, I see the point of view here, and am inclined to agree with what Tucker says
below:

[Previous message was quoted here - Editor.]

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

From: Bob Duff
Date: Friday, April 30, 2010  5:55 PM

>    2) Simple expression-level predicates in the private part.

What I don't get is why "simple" should mean exactly "one expression".
I mean, declaring my one little Square constant (see other e-mail) doesn't imply
any complexity.  OTOH, an expression can look at globals, so it's not
necessarily "simple" from an analysis point of view.

Shrug.  I guess I see small payoff for this feature -- but I agree with Randy
and Tuck that the cost is also fairly small.  We're just disagreeing on the
ratio.

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

From: Robert Dewar
Date: Friday, April 30, 2010  6:04 PM

> Shrug.  I guess I see small payoff for this feature -- but I agree
> with Randy and Tuck that the cost is also fairly small.  We're just
> disagreeing on the ratio.

Of course if you put in LET, then you are close to a full expressioun language,
and if you put in LAMBDA, you are all the way there :-)

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

From: Bob Duff
Date: Friday, April 30, 2010  6:03 PM

> Sorry about the interruptions. I think you were pausing to gather your
> thoughts long enough that we thought you were done talking.

Yeah, that's a fault of mine -- I can't think quickly when speaking to people,
so I pause, so people jump in, and that causes me to get even more distracted...

That's why I prefer e-mail for most technical communication.

Of course, face-to-face meetings are better than phone meetings, because you can
see visual cues about who wants to speak when.
That's why I like to go to SofCheck for the ARG phone meetings
-- at least I see ONE person face to face.

> I don't see any way to accomplish a significantly less restrictive vision.
> Honestly, I don't see much point (beyond the easier inlining) to doing
> this for anything other than predicates. For the sorts of functions
> that occur as predicates, either they are trivial combinations of
> component values, or they require some complex operations that have no
> advantage to being exposed anyway.
>
> For instance, if you need a local variable and a loop to implement a
> predicate, it's not very likely to be analyzable anyway.

How about a local constant, and no loop?

function Is_Good (X, Y : Integer) return Boolean
    renames X * X > Y and X * X + 1 <= Y + Blah;

versus:

function Is_Good (X, Y : Integer) return Boolean is
    Square : constant Integer := X * X;
begin
    return Square > Y and Square + 1 <= Y + Blah; end Is_Good;

or (to mix in some Lisp-y syntax):

function Is_Good (X, Y : Integer) return Boolean
     renames (let Square = X * X
        in (Square > Y and Square + 1 <= Y + Blah));

Anyway, part of my point is that "not very likely to be analyzable"
is not something we are in a position to judge.  It depends on tools that have
not yet been designed.

...
> > It's fine with me if some tools (possibly optionally) look at
> > private parts.
> > But if they do, they might as well look at bodies, too.
> > Conceptually, private part and body are both part of the
> > "implementation"; only the visible part is "specification".
> > In fact, they might as well look at all type extensions of a given
> > root type.  That's what's needed to "expose the implementation" in
> > all cases.  So I don't see any advantage to expression functions,
> > for tools that wish to break privacy.
> >
> > But a modular analysis of a client should look only at visible parts
> > of whatever it calls.
>
> Ada allows children to have visibility on the private part, so it's
> not correct to claim that no one should look there.

I didn't say "no one".  I said "clients".  Children are not clients -- they are
part of the abstraction.  (In fact, if I ran the circus, children would see
parent bodies.)

>...Compilers look there all the
> time, ...

Never for legality checks.  Only for code gen.  And for code gen, compilers look
at bodies (for inlining, and for generic instantiation (except in the case of
your generic-sharing implementation)).

>...and the runtime correctness of a program *depends* on what is found
>there. And what we're trying to analyze is the runtime correctness,
>isn't  it??

Well, yeah, sort of.  But a modular analysis that doesn't break privacy is more
useful -- it means the analysis will still be correct if you change the
implementation.

In other words, a proof that says "this thing won't raise C_E in this program"
is useful, but a proof that says, "this thing won't raise C_E, period, no matter
what calls it or is called by it" is MORE useful.

The main point of putting various assertions on specs (like preconditions) is to
enable the latter more-useful kind of analysis.

> In any case, I think the most important thing is to allow *compilers*
> to be able to do these sorts of analyses, without having to depend on
> anything that they don't naturally have. A compiler always has access
> to the private part of a package, and rarely has access to a body
> other than the one being compiled. Compilers usually don't pay much
> attention to privacy once they've gotten the legality rules out of the
> way - I don't think our compiler does any analysis on the code
> whatsoever until after the stage where privacy and the like is
> respected. (And of course there are runtime considerations which
> require ignoring privacy.)
>
> Why do I think compilers are so important? It's not so much compilers
> as whatever is the first tool run on the source code to remove errors.
> It should be possible to find the maximum number of errors immediately
> after finishing writing the code for a single unit, because that's
> when they're easiest to fix. These days, the first tool run is almost
> always the compiler (at least to do deep analysis - some IDEs do some
> syntactic checking). For that to work, no other units other than
> direct dependencies (in particular, no bodies) need exist.
>
> The other, related issue for me is that compilers have to be able to
> eliminate most of these contracts in the same way that we eliminate
> most range checks. Like range checks, turning off contracts is like
> using seat belts until you leave the garage - it's something you shouldn't do.

Bad analogy: seat belts cost near-zero to use.

...
> > My final point here is that I think globals annotations are a more
> > fruitful endeavor.  As proposed, they're not ready to be
> > standardized, but I think implementations can experiment with them,
> > and should give that experimentation higher priority than expression
> > functions.

> You are for some reason equating things that have very different
> orders of magnitude. Expression functions probably will take a week or
> so of effort to implement. Globals annotations are at least an order
> of magnitude more effort (probably two orders).

Yes, I agree that expression functions are much simpler to implement (and to
define the semantics of) than globals annotations.

...
> I don't agree that the framework for globals annotations is not ready
> to be standardized. The specific annotations that work best probably
> will require some experimentation, but by not putting together a
> common framework populated with a few important annotations which are
> obvious (specific items, everything in a package, nothing at all),
> we're either going to end up with a tower-of-babble or just as likely
> nothing at all. Even so, I understand why people feel this way and am
> willing to go without. But what I will not stand for is having
> supposed contracts with no way whatsoever for the compiler to analyze
> them if they're written only in portable Ada. If we don't have one or
> the other, then I don't want ANY new contracts in Ada. And I am going to fight
> that battle as long as I can.

I don't see why you want to pound your shoe on the table in this way.
I mean, preconditions and predicates are useful even if they are just run-time
checks, with no "proof tools" in sight.

You have to look at the alternative:  Put comments, which are obviously not
checked at all.

...
> You are always telling us to not let "best" prevent us from adopting a
> solution that is "good enough". Here is a solution that is good enough
> for 80% of predicate functions, lets compilers at least have the
> information they need, has very little cost since there is hardly
> anything new here (just a new combination of existing pieces). You're
> saying that we can't have this solution because it isn't "best". And
> *then* you go on and say we can't have the "best" solution either
> because it needs more study. I can't imagine a more classic example of letting
> "best" kill off "good enough"!!

Your honor, I plead guilty as charged.

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

From: Bob Duff
Date: Friday, April 30, 2010  6:15 PM

> I think I agree with Randy that this is a simple feature ...

I agree it's a simple feature.

>...which will make a significant pragmatic  difference in the ability
>for compilers to do  additional compile-time analysis.

That part, I doubt.

I don't see how knowing that Is_Empty means "Blah.Count = 0" helps, unless the
compiler knows all places where the private Count component is modified.  That
requires looking at the body, not just the private part.

And compilers already know how to look at bodies (for inlining), so I don't see
any benefit from moving information from the body to the private part.

>...  After all, in Ada 83,
> there was no real reason to have a private part,

You can stop right there.  ;-)

> except for pragmatic reasons associated with separate compilation.
> The private part is exactly those things you need to provide the
> compiler when compiling a *client* of an abstraction, to allow the
> compiler to generate efficient code.

Efficient code has little to do with static analysis.

And anyway, efficient code requires inlining bodies, sometimes.

...
> As an example of existing private-part information that might affect
> compile-time warnings, consider whether a private type includes full
> default initialization.  If the private type is implemented with a
> scalar type, then no default initialization is provided.  If it is
> implemented with an access type, then it is default initialized to
> null.
> If it is implemented using a composite type, then how much of it is
> default initialized varies according to information that is specified
> in the private part.
>
> Clearly if you write:
>
>     X : Priv_Type;
>     Default_Value : constant Priv_Type := X;
>
> it would make sense for the compiler to provide a compile-time warning
> if Priv_Type is in fact implemented with a scalar type (or an
> array-of-scalar).

Yes, I agree.  That's because there's a flaw in Ada: you can't know from the visible part whether it makes sense to declare a default-initialized object of type Priv_Type.

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

From: Randy Brukardt
Date: Friday, April 30, 2010  6:42 PM

...
> > For instance, if you need a local variable and a loop to implement a
> > predicate, it's not very likely to be analyzable anyway.
>
> How about a local constant, and no loop?
>
> function Is_Good (X, Y : Integer) return Boolean
>     renames X * X > Y and X * X + 1 <= Y + Blah;
>
> versus:
>
> function Is_Good (X, Y : Integer) return Boolean is
>     Square : constant Integer := X * X; begin
>     return Square > Y and Square + 1 <= Y + Blah; end Is_Good;
>
> or (to mix in some Lisp-y syntax):
>
> function Is_Good (X, Y : Integer) return Boolean
>      renames (let Square = X * X
>         in (Square > Y and Square + 1 <= Y + Blah));

I thought about this when I wrote my original reply, and it stuck me that for
*constants* you might as well just define a second expression function. One
presumes the constant has some well-defined meaning (if it doesn't, how could
you name it and why would you want it?); it's unlikely to hurt to be more
generally available.

That is, I'd say that you should write:

function Square (X : Integer) return Integer renames (X * X);

function Is_Good (X, Y : Integer) return Boolean is (Square(X) > Y and
Square(X) + 1 <= Y + Blah);

Presuming inlining, it will generate the same code either way; the amount of
text is about the same either way.

I didn't think this really answered your concern properly, so I didn't put it
into my reply. But maybe I was right the first time...

> Anyway, part of my point is that "not very likely to be analyzable"
> is not something we are in a position to judge.  It depends on tools
> that have not yet been designed.

This is true, of course.

...
> >...Compilers look there all the
> > time, ...
>
> Never for legality checks.  Only for code gen.  And for code gen,
> compilers look at bodies (for inlining, and for generic instantiation
> (except in the case of your generic-sharing implementation)).

Well, all of these things are technically done at runtime. There aren't any
legality checks involved. Yes, I realize this is Ada lawyer hairsplitting.

> >...and the runtime correctness of a program *depends* on what is
> >found there. And what we're trying to analyze is the runtime
> >correctness, isn't  it??
>
> Well, yeah, sort of.  But a modular analysis that doesn't break
> privacy is more useful -- it means the analysis will still be correct
> if you change the implementation.
>
> In other words, a proof that says "this thing won't raise C_E in this
> program"
> is useful, but a proof that says, "this thing won't raise C_E, period,
> no matter what calls it or is called by it" is MORE useful.

I can't argue with this. But I don't think I want to have to wait until 2025 to
be able to get anything, and as Tucker says, proofs based only on specs are
beyond the state of the art today (at least for full-size programming languages
like Ada).

...
> > The other, related issue for me is that compilers have to be able to
> > eliminate most of these contracts in the same way that we eliminate
> > most range checks. Like range checks, turning off contracts is like
> > using seat belts until you leave the garage - it's
> something you shouldn't do.
>
> Bad analogy: seat belts cost near-zero to use.

This analogy is used for range checks all the time. The point is that with
effort, the compiler can make the cost of range checks near-zero.

I think this is an important property of contracts (as opposed to just runtime
assertions, which definitely don't have this property): the compiler ought to be
able to eliminate the majority of the checks. (And the ones that remain suggest
places where the program might have problems.)

If contracts are expensive, no one will use them in the first place. But they're
an important safety feature, so they need to be reasonably cheap. And in any
case turning off safety devices to go out in the world is silly. That's when you
*need* safety devices - to deal with the unforeseen!

(This expense argument is often used against Ada's range and other checks, but
we Ada people know from experience that it is rare that a program has a
performance problem specifically because of the presence of these checks.
Usually the program is plenty fast whether or not they are on, or it is too slow
either with them on or turned off. You can make the same argument about size of
checks. Ada provides Suppress for the rare program in the middle, not for some
sort of general need. All of this applies just as well to all contracts -- and
in large part to assertions as well. [The vast majority of assertions in my code
are just a normal part of the code; I don't make any effort to be able to turn
them off. Why compile/serve web pages/analyze spam without seat belts??])

...
> > I don't agree that the framework for globals annotations is not
> > ready to be standardized. The specific annotations that work best
> > probably will require some experimentation, but by not putting
> > together a common framework populated with a few important
> > annotations which are obvious (specific items, everything in a
> > package, nothing at all), we're either going to end up with a
> > tower-of-babble or just as likely nothing at all. Even so, I
> > understand why people feel this way and am willing to go without.
> > But what I will not stand for is having supposed contracts with no
> > way whatsoever for the compiler to analyze them if they're written
> > only in portable Ada. If we don't have one or the other, then I
> > don't want ANY new contracts in Ada. And
> I am going to fight that battle as long as I can.
>
> I don't see why you want to pound your shoe on the table in this way.
> I mean, preconditions and predicates are useful even if they are just
> run-time checks, with no "proof tools" in sight.

Sure, but we don't need new features for that; putting pragma Assert inside of a
subprogram body will provide that just fine. (Or just using ordinary code, as we
do in Claw.)

The promise of these new features is for them to be at least partially
compile-time checkable, with little or no runtime overhead. That's highly
unlikely to happen for pragma Assert (or anything in the body, for that matter).

> You have to look at the alternative:  Put comments, which are
> obviously not checked at all.

No, the alternative is using pragma Assert and/or ordinary code in the
subprogram body. Still checked, but not well communicated to the caller. We have
a name for people who don't check boundary conditions: "C programmers" ;-)

...
> > You are always telling us to not let "best" prevent us from adopting
> > a solution that is "good enough". Here is a solution that is good
> > enough for 80% of predicate functions, lets compilers at least have
> > the information they need, has very little cost since there is
> > hardly anything new here (just a new combination of existing
> > pieces). You're saying that we can't have this solution because it
> > isn't "best". And
> > *then* you go on and say we can't have the "best" solution either
> > because it needs more study. I can't imagine a more classic
> example of letting "best" kill off "good enough"!!
>
> Your honor, I plead guilty as charged.

I sentence you to getting your homework done early. :-)

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

From: Robert Dewar
Date: Friday, April 30, 2010  7:06 PM

>> ...  After all, in Ada 83,
>> there was no real reason to have a private part,
>
> You can stop right there.  ;-)
>
>> except for pragmatic reasons associated with separate compilation.
>> The private part is exactly those things you need to provide the
>> compiler when compiling a *client* of an abstraction, to allow the
>> compiler to generate efficient code.

Pretty fundamental "pragmatic reasons", the compiler HAS to know the layout of
types, to allocate space for them if nothing else!

> Efficient code has little to do with static analysis.

True indeed

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

From: Bob Duff
Date: Friday, April 30, 2010  7:46 PM

> Pretty fundamental "pragmatic reasons", the compiler HAS to know the
> layout of types, to allocate space for them if nothing else!

It doesn't HAVE to.  It HAS to only for efficiency reasons.

And for maximal efficiency, it has to do inlining, which
(currently) requires looking at bodies.  I don't think the sky would fall if
compilers also had to take a peek at bodies in order to efficiently allocate
space for objects of private types.

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

From: Roberrt Dewar
Date: Friday, April 30, 2010  8:20 PM

I strongly disagree, avoiding dynamic allocation is not just an efficiency
issue, it is a fundamental functional issue in certified environments that do
not allow dynamic allocation.

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

From: Bob Duff
Date: Friday, April 30, 2010  7:32 PM

> I thought about this when I wrote my original reply, and it stuck me
> that for *constants* you might as well just define a second expression function.
> One presumes the constant has some well-defined meaning (if it
> doesn't, how could you name it and why would you want it?); it's
> unlikely to hurt to be more generally available.
>
> That is, I'd say that you should write:
>
> function Square (X : Integer) return Integer renames (X * X);
>
> function Is_Good (X, Y : Integer) return Boolean is (Square(X) > Y and
> Square(X) + 1 <= Y + Blah);

Good point.

> Presuming inlining, it will generate the same code either way; the
> amount of text is about the same either way.

Agreed.

> I didn't think this really answered your concern properly, so I didn't
> put it into my reply. But maybe I was right the first time...

Yes, you were right the first time.  ;-)

I learned something.

> I can't argue with this. But I don't think I want to have to wait
> until 2025 to be able to get anything, and as Tucker says, proofs
> based only on specs are beyond the state of the art today (at least
> for full-size programming languages like Ada).

Well, Tuck's CodePeer tool looks at bodies (transitively) but it does so by
generating automatically the preconditions and the globals annotations that
we're discussing.

So I think "beyond state of the art" doesn't mean "the tools aren't smart
enough", but more like "the tools don't have the information they need".  We're
trying to give them that info.

> ...
> > > The other, related issue for me is that compilers have to be able
> > > to eliminate most of these contracts in the same way that we
> > > eliminate most range checks. Like range checks, turning off
> > > contracts is like using seat belts until you leave the garage -
> > > it's
> > something you shouldn't do.
> >
> > Bad analogy: seat belts cost near-zero to use.
>
> This analogy is used for range checks all the time.

Yeah, I know.  Or similar analogies involving floatation devices for sailors,
and parachutes for airplane pilots. I'm not picking on you -- I think it's
equally bogus when Tony Hoare does such reasoning-by-sound-bite.  ;-)

>... The point is that with
> effort, the compiler can make the cost of range checks near-zero.

Sometimes, other times not.

> I think this is an important property of contracts (as opposed to just
> runtime assertions, which definitely don't have this property): the
> compiler ought to be able to eliminate the majority of the checks.
> (And the ones that remain suggest places where the program might have
> problems.)

I think you're using "contract" in a non-standard way.
Eiffel's contracts are just run-time checks, just like ours are

> If contracts are expensive, no one will use them in the first place.

Nonsense.  If something is too expensive for production use, it can still be
useful for testing.

>...But
> they're an important safety feature, so they need to be reasonably cheap.

No, they don't need to be.  We would like them to be.

> And in any case turning off safety devices to go out in the world is silly.
> That's when you *need* safety devices - to deal with the unforeseen!

Nonsense again.  Turning off "safety devices" is an engineering decision based
on costs/benefit.

> (This expense argument is often used against Ada's range and other
> checks,

I agree that range checks are analogous.

> ...
> > I don't see why you want to pound your shoe on the table in this way.
> > I mean, preconditions and predicates are useful even if they are
> > just run-time checks, with no "proof tools" in sight.
>
> Sure, but we don't need new features for that; putting pragma Assert
> inside of a subprogram body will provide that just fine. (Or just
> using ordinary code, as we do in Claw.)

No, it isn't "just fine".  Preconditions get scattered about all callers automatically.  That's useful, even if unsound.

> The promise of these new features is for them to be at least partially
> compile-time checkable, with little or no runtime overhead. That's
> highly unlikely to happen for pragma Assert (or anything in the body,
> for that matter).
>
> > You have to look at the alternative:  Put comments, which are
> > obviously not checked at all.
>
> No, the alternative is using pragma Assert and/or ordinary code in the
> subprogram body. Still checked, but not well communicated to the
> caller. We have a name for people who don't check boundary conditions: "C
> programmers" ;-)

OK, but preconditions are still better than that (sprinkle checks in various
useful places, compared to the programmer sprinkling Assert in some of those
places).

> ...
> > > You are always telling us to not let "best" prevent us from
> > > adopting a solution that is "good enough". Here is a solution that
> > > is good enough for 80% of predicate functions, lets compilers at
> > > least have the information they need, has very little cost since
> > > there is hardly anything new here (just a new combination of
> > > existing pieces). You're saying that we can't have this solution
> > > because it isn't "best". And
> > > *then* you go on and say we can't have the "best" solution either
> > > because it needs more study. I can't imagine a more classic
> > example of letting "best" kill off "good enough"!!
> >
> > Your honor, I plead guilty as charged.
>
> I sentence you to getting your homework done early. :-)

Yes, sir, your honor, sir!  ;-)

Seriously, I hope to do it tomorrw or Sunday.  Thank you very much for providing
the relevant meeting notes!  (which I have not yet looked at)

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

From: Robert Dewar
Date: Friday, April 30, 2010  8:18 PM

>> If contracts are expensive, no one will use them in the first place.
>
> Nonsense.  If something is too expensive for production use, it can
> still be useful for testing.

Machines are so fast, that for many users, CPU time is simply not a limited
resource.

>> ...But
>> they're an important safety feature, so they need to be reasonably cheap.
>
> No, they don't need to be.  We would like them to be.
>
>> And in any case turning off safety devices to go out in the world is silly.
>> That's when you *need* safety devices - to deal with the unforeseen!
>
> Nonsense again.  Turning off "safety devices" is an engineering
> decision based on costs/benefit.

Furthermore, leaving in run-time checks for production builds can be MUCH more
dangerous than omitting them, if you haven't carefully figured out what to do if
a check fails. Ariane-5 is a really good example of this.

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

From: Randy Brukardt
Date: Friday, April 30, 2010  8:34 PM

...
> > > I don't see why you want to pound your shoe on the table in this way.

It's interesting that "pound your shoe" has become a synonym for "take an
extreme" position within the Ada community. I generally keep my shoes on...

> > > I mean, preconditions and predicates are useful even if they are
> > > just run-time checks, with no "proof tools" in sight.
> >
> > Sure, but we don't need new features for that; putting pragma Assert
> > inside of a subprogram body will provide that just fine. (Or just
> > using ordinary code, as we do in Claw.)
>
> No, it isn't "just fine".  Preconditions get scattered about all
> callers automatically.  That's useful, even if unsound.

Sorry, I was talking about putting the Asserts/other code inside the called
subprogram body. I agree that putting those at the call site is not "just fine".
But there is no reason to put those at the call site for the purposes of runtime
checks -- all that does is bloat up the code. The purpose of putting them at the
call site is to enable optimization/static checking; if you're not doing that,
you have no reason to not put them inside of the body.

> > The promise of these new features is for them to be at least
> > partially compile-time checkable, with little or no runtime
> > overhead. That's highly unlikely to happen for pragma Assert (or
> > anything in the body, for that matter).
> >
> > > You have to look at the alternative:  Put comments, which are
> > > obviously not checked at all.
> >
> > No, the alternative is using pragma Assert and/or ordinary code in
> > the subprogram body. Still checked, but not well communicated to the
> > caller. We have a name for people who don't check boundary
> conditions: "C programmers"
> > ;-)
>
> OK, but preconditions are still better than that (sprinkle checks in
> various useful places, compared to the programmer sprinkling Assert in
> some of those places).

No sprinkling going on; those checks are in the called body, not at the call
site, and surely are going to occur in every call for that reason.

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

From: Randy Brukardt
Date: Friday, April 30, 2010  8:45 PM

Oops, missed one comment.

...
> > I think this is an important property of contracts (as opposed to
> > just runtime assertions, which definitely don't have this property):
> > the compiler ought to be able to eliminate the majority of the checks.
> > (And the ones that remain suggest places where the program might
> > have
> > problems.)
>
> I think you're using "contract" in a non-standard way.
> Eiffel's contracts are just run-time checks, just like ours are

I probably am; see my paper on this topic. I needed a way to differentiate pure
runtime checks (which I called "assertions") from checks that can usefully be
analyzed statically (which I called "contracts"). Maybe there is a better term
for the latter, but that is always what I meant by "contracts" (including in the
ARG instructions). The big benefit of using Ada is the many ways that Ada
detects problems and refuses to let you proceed until they're fixed; runtime
checks are of much less benefit (which is not to say NO benefit!) as they
require extensive testing to trigger problems and cause what you call a
"tripping hazard" in fielded systems.

Using this terminology: I'm not interested in any more "assertions" in Ada (that
is, pure runtime checks); if we get some because of people writing bad
contracts, that's OK, but they are nearly pointless. (I have more sympathy for
predicate assertions, because "sprinkling" those is hard;
precondition/postcondition assertions on the other hand are pretty simple to
write in the body and I suspect most of us have been writing those since the
early days of Ada 83).

My preference would be for contracts with real legality rules (like we have for
parameter passing, generic instantiation, and the like), but that's probably
unrealistic for anything beyond "set constraints". So I'll live with ones that
can be reduced/detected as warnings of one sort of another.

My understanding of Eiffel is that it doesn't have any real contracts beyond
subprogram profiles.

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

From: Robert Dewar
Date: Friday, April 30, 2010  8:54 PM

>>>> I don't see why you want to pound your shoe on the table in this way.
>
> It's interesting that "pound your shoe" has become a synonym for "take
> an extreme" position within the Ada community. I generally keep my shoes on...

It means that in any context, it comes from Kruschev and the U-2 affair!

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

From: Bob Duff
Date: Friday, April 30, 2010  9:04 PM

> It's interesting that "pound your shoe" has become a synonym for "take
> an extreme" position within the Ada community. I generally keep my shoes on...

Sorry.  When I say "pound one's shoe on the table" I am accusing you of being
somewhat over-the-top in your rhetoric, either for or against some technical
position.  It's a reference to the famous case where Nikita Khrushchev of the
Soviet Union actually pounded his shoe on the table to make a point (whetever
point it was, I don't much care) in a United Nations debate.

There's a description of it here:

http://en.wikipedia.org/wiki/Shoe-banging_incident

So when you say, for example, "that's a nonstarter" or "that is unacceptable", I
respond that "you're pounding your shoe on the table".  Get it?

When you say, "I don't like that" or "I think that causes maintenance problems",
then I won't cry "shoe on table".  ;-)

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

From: Robert Dewar
Date: Friday, April 30, 2010  8:57 PM

>> I think you're using "contract" in a non-standard way.
>> Eiffel's contracts are just run-time checks, just like ours are
>
> I probably am; see my paper on this topic. I needed a way to
> differentiate pure runtime checks (which I called "assertions") from
> checks that can usefully be analyzed statically (which I called
> "contracts"). Maybe there is a better term for the latter, but that is always
> what I meant by "contracts"

That's REALLY confusing terminology. As Bob says, the word contract is strongly
associated with Ada (as in the trademarked phrase programming by contract) and
in this context it ALWAYS refers to run-time checks.

> Using this terminology: I'm not interested in any more "assertions" in
> Ada (that is, pure runtime checks); if we get some because of people
> writing bad contracts, that's OK, but they are nearly pointless. (I
> have more sympathy for predicate assertions, because "sprinkling"
> those is hard; precondition/postcondition assertions on the other hand
> are pretty simple to write in the body and I suspect most of us have
> been writing those since the early days of Ada 83).

To say that contracts as used in Eiffel are nearly pointless is provocative and
is definitely an extreme minority position. And for sure we have lots of major
Ada users who are VERY interested in contracts in the normal sense, as Eiffel
defines it.

> My preference would be for contracts with real legality rules (like we
> have for parameter passing, generic instantiation, and the like), but
> that's probably unrealistic for anything beyond "set constraints". So
> I'll live with ones that can be reduced/detected as warnings of one sort of another.
>
> My understanding of Eiffel is that it doesn't have any real contracts
> beyond subprogram profiles.

Well you are using contracts in such a confusing manner that I don't know what
to make of such a comment!

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

From: Yannick Moy
Date: Saturday, May 1, 2010  2:28 AM

>> I probably am; see my paper on this topic. I needed a way to
>> differentiate pure runtime checks (which I called "assertions") from
>> checks that can usefully be analyzed statically (which I called
>> "contracts"). Maybe there is a better term for the latter, but that
>> is always what I meant by "contracts"
>
> That's REALLY confusing terminology. As Bob says, the word contract is
> strongly associated with Ada (as in the trademarked phrase programming
> by contract) and in this context it ALWAYS refers to run-time checks.

I think the term "contract" is meaning the two things for different groups of
people. Historically, it means the run-time checking as performed in Eiffel, and
it still means this for most people. In the research community of program
proving, it means of course what Randy means: side-effect free deterministic
terminating boolean expressions.

JML and Spec# take the word of the programmer for it, as only methods marked as
"pure" in the source can be called from contracts, where pure means essentially
side-effect free. Here is the JML definition of pure:

http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_7.html#SEC59

SPARK allows calls to SPARK functions (which cannot have side-effects anyway)
and logic functions (declared in stylized comments and defined in Prolog syntax
for the prover).

ACSL only allows calls to logic functions, either defined in stylized comments
(which look a lot like expression functions), or only declared in stylized
comments and defined by some axiomatic. Here is the ACSL definition of
expressions used in contracts (section 2.2):

http://frama-c.com/download/acsl_1.4.pdf

I think it is less confusing to speak about contracts in the Eiffel way, while
working towards making these contracts amenable to static analysis.

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

From: Robert Dewar
Date: Saturday, May 1, 2010  5:38 AM

> I think the term "contract" is meaning the two things for different
> groups of people. Historically, it means the run-time checking as
> performed in Eiffel, and it still means this for most people.

Given the trademarked phrase, I think that's the only way it should be used. How
about using the phrase "static contracts" when we mean that and "dynamic
contracts" when we mean that, so we never get confused. Of course part of the
goal is in some cases to have contracts that can be regarded as either static or
dynamic (that would be true in Eiffel too, to the extent that Eiffel contracts
can be treated statically, it would make sense to do so).

> In the research community of program
> proving, it means of course what Randy means: side-effect free
> deterministic terminating boolean expressions.

(side comment on side-effect free)

I never know what side-effect free means, for instance the only possible
reasonable implementation of a function like Ackerman is to memoize. Does the
memoization of such a function make it have a side effect, or is it just an
efficiency detail of the implementation (in some languages you get the
memoization effect just by asking for it without having to program it, and there
you can most clearly see it is just an low level im-plementation detail, whereas
in this kind of context side-effect free is a high level semantic concept.

Or if you add a counter to a square root function so that for tuning purposes
you can tell how many times it is called, then it is still conceptually pure,
and indeed you want the compiler still to hoist calls, eliminate duplicate calls
etc.

During the discussion of Ada 83, there was some considerable sentiment for
distinguishing between side effect free functions and value returning procedures
(a la the DEC pragma). But the discussion ALWAYS got bogged down in discussions
of points like these, and never got anywhere.

And of course all functions have side effects if you think in terms of the stack
usage, needing to allocate stack space (and possibly raising SE), not to mention
leaving traces of the call on the stack.

So for my taste, one should avoid the phrase side-effect free and instead use a
well defined term in its place that specifies the semantic level at which this
property is defined.

> SPARK allows calls to SPARK functions (which cannot have side-effects
> anyway) and logic functions (declared in stylized comments and defined
> in Prolog syntax for the prover).

Of course at the low level of looking at memory usage, all SPARK functions *do*
have side effects, and indeed when the claim is made that a program has been
proved to be run-time exception free, this does not cover Storage_Error! That
has to be verified at a totally different level.

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

From: Tucker Taft
Date: Saturday, May 1, 2010  8:02 AM

>> ...
>> Efficient code has little to do with static analysis.
>
> True indeed

This one surprises me.  Efficient Ada code implies eliminating unnecessary
run-time checks.  Good static analysis (e.g. range propagation)is normally the
key to that.  Now that we have user-written assertions, preconditions,
postconditions, etc., eliminating unnecessary the checks associated with these
requires even more static analysis.

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

From: Robert Dewar
Date: Saturday, May 1, 2010  8:20 AM

Yes, of course, but what we (or at least I) meant by this is that issues of
efficient code generation are not relevant to the *process* of static analysis,
though indeed the *results* of static analysis most certainly can lead to better
code generation (e.g. not generating code for dead code that is not obviously
dead without subtle analysis).

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

From: Bob Duff
Date: Saturday, May 1, 2010  10:29 AM

Right, me too.

Also, there are some important differences between static analysis done to make
sure the program works, versus making it fast.

For the former, you prefer to be modular (clients don't depend on private parts
and bodies), so the analysis of one thing can't be invalidated by changes in the
other.  For the latter, it's just fine to depend on bodies -- that's what
inlining is all about.

The world desperately needs the former.  For the latter, well, shrug, lots of
programs are plenty fast enough as it is, and besides, we already have a
solution for slow run-time checks -- suppress them.  (Don't start shoe pounding
-- I'm well aware of the costs and benefits of suppressing checks, and I don't
buy analogies with seat belts and life jackets).

If static analysis can make programs faster without resorting to Suppress,
that's a nice side effect, but I have zero interest in discussing how to design
our assertions to accomplish that.

P.S. Note to Randy on terminology: "Assertions" includes pragma Assert,
pre/post-conditions, invariants, null exclusions, constraints, predicates.  (I'm
saying this because you asserted during the meeting that "assertion" means only
pragma Assert.)  "Contract" means that subset of assertions that are visible to
clients. This is pretty well established terminology (see e.g. Bertrand Meyer's
writings), so I suggest we not try to change it.

And both terms (assertion and contract) are broad -- they don't imply static
versus dynamic checking (could be some of both).  This part is admittedly not
universal (some static analysis zealots claim that an "assertion" must be
statically checked, or it's not an assertion -- but they're wrong. ;-) )

Even a comment can be called an assertion.  And if it's in the spec, it can be
called part of the contract.  Those are checked only by "code review".

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

From: Bob Duff
Date: Saturday, May 1, 2010  11:23 AM

> Given the trademarked phrase, I think that's the only way it should be
> used. How about using the phrase "static contracts" when we mean that
> and "dynamic contracts" when we mean that, so we never get confused.

I think "contract" means an expression of some property that one piece of code
agrees to ensure, so another piece of code can rely on it.

"Static" and "dynamic" should not be viewed as properties of a contract, but as
properties of various tools that automatically check them (or even human beings
who check them "by hand").

> Of course part of the goal is in some cases to have contracts that can
> be regarded as either static or dynamic (that would be true in Eiffel
> too, to the extent that Eiffel contracts can be treated statically, it
> would make sense to do so).

Right, exactly.

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

From: Tucker Taft
Date: Saturday, May 1, 2010  8:22 AM

I think it might be useful to refer to these two different proposals as:

   Parameterized Expressions

and

   Bodies in Specs

I personally have an interest in Parameterized Expressions, but no interest in
Bodies in Specs.

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

From: Robert Dewar
Date: Saturday, May 1, 2010  8:28 AM

> I personally have an interest in Parameterized Expressions, but no
> interest in Bodies in Specs.

I don't think these are so separate, bodies-in-specs is intended to address
exactly the same issues as renamed expressions, just in a more general form, so
I don't think it is helpful to try to separate two solutions for the same
problem.

I do have some sympathy for Tuck's objections to bodies in specs as confusing,
and for sure the potential for abuse is huge:

"what's all this crap about specs and bodies? let's just put everything in the
specs and avoid this nonsense!"

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

From: Bob Duff
Date: Saturday, May 1, 2010  10:44 AM

> I do have some sympathy for Tuck's objections to bodies in specs as
> confusing, and for sure the potential for abuse is huge:

I agree with you and Tuck that the potential for abuse is huge.

But I have zero sympathy for Tuck's objections -- "potential abuse"
is NEVER an appropriate language-design criterion.  "Potential for accidental
misuse" is, but not mere "potential abuse".

This example illustrates why.  Tuck wants to prevent "abuse", but he can't
define that precisely, so he defines "abuse" as "putting anything besides an
expression in the spec", which is just a wrong definition.  It prevents some
(not all) misuse, but also prevents legitimate use (like my example of a local
constant).  My definition is "putting large, complicated stuff in the spec" --
but that's not precise enough for a language rule.

> "what's all this crap about specs and bodies? let's just put
> everything in the specs and avoid this nonsense!"

Sure -- the same folks who think every type should have a non-portable rep
clause, or unchecked conversions should be scattered all over the place, etc.
It's not our job as language designers to rein in those folks.  It's your job as
an NYU prof to educate them.  ;-)

Having said all that, I must admit that my objections to parameterized
expressions are weak.  I'm not going to quit using Ada if this feature is added.
In fact, I would use this feature myself, if it existed.

I also admit that it's easy to implement.

P.S. I don't understand why the term "parameterized expressions"
is preferable to "expression functions" -- I don't much care.

P.P.S. Tucker suggested a similar thing for a procedure, which I imagine looks
like this:

    procedure Blah (X : T);
  private
    procedure Blah (X : T) renames
      Mumble(X*X); -- A single procedure call goes here.

So what's the term for that?

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

From: Robert Dewar
Date: Saturday, May 1, 2010  11:58 AM

> But I have zero sympathy for Tuck's objections -- "potential abuse"
> is NEVER an appropriate language-design criterion.  "Potential for
> accidental misuse" is, but not mere "potential abuse".

For me, I never say never! And in this case, I think the potential for confusion
and abuse is too high compared to the utility.

I do think that potential abuse is a legitimate consideration.
For example, suppose we argued to introduce completely unsafe untyped pointers
to solve some very specific problem with the understanding that they should only
be used in this situation. I would object that it would simply be too easy for
people to abuse this feature.

Unchecked_Union is an interesting example for me of a feature on the edge. You
can easily see it being abused, but I think we are safe given its very specific
descriptyion as being for interfacing with C unions.

> This example illustrates why.  Tuck wants to prevent "abuse", but he
> can't define that precisely, so he defines "abuse"
> as "putting anything besides an expression in the spec", which is just
> a wrong definition.  It prevents some (not all) misuse, but also
> prevents legitimate use (like my example of a local constant).  My
> definition is "putting large, complicated stuff in the spec" -- but
> that's not precise enough for a language rule.

I would prefer to solve the local constant problem by introducing LET.

>> "what's all this crap about specs and bodies? let's just put
>> everything in the specs and avoid this nonsense!"
>
> Sure -- the same folks who think every type should have a non-portable
> rep clause, or unchecked conversions should be scattered all over the
> place, etc.

No, I don't buy the analogy in this case, I don't think these cases are similar.

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

From: Bob Duff
Date: Saturday, May 1, 2010  12:43 PM

> For me, I never say never!

I rarely do.  ;-)

> I would prefer to solve the local constant problem by introducing LET.

If we can come up with a good syntax for it, then that seems like a reasonable
solution.

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

From: Tucker Taft
Date: Saturday, May 1, 2010  1:20 PM

> I agree with you and Tuck that the potential for abuse is huge.
>
> But I have zero sympathy for Tuck's objections -- "potential abuse"
> is NEVER an appropriate language-design criterion.  "Potential for
> accidental misuse" is, but not mere "potential abuse"...

Well, here we differ.  I believe that part of good language design is
"encouraging" the programmer to make wise choices, by making some things easier
than others.  Just giving programmers free and uniform license to do whatever
they want is a design philosophy, but it isn't mine.  Of course there is a
spectrum here, but I think you (Bob) and I are on somewhat different places on
this spectrum.

So for me, if a feature has more "potential for abuse"
than some other feature, I will favor the one with less such potential, and not
surprisingly that will sometimes "crimp" someone's style.  If it doesn't do that
now and then, it is probably too lax in my book.

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

From: Robert Dewar
Date: Saturday, May 1, 2010  1:28 PM

So I seem to be somewhere in between, on this issue I tend to side with Tuck,
but when it comes to IN OUT parameters in functions, I would be happy to allow
them without the complexification of the anti-side effect rule.

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

From: Robert Dewar
Date: Saturday, May 1, 2010  1:26 PM

>> I would prefer to solve the local constant problem by introducing
>> LET.
>
> If we can come up with a good syntax for it, then that seems like a
> reasonable solution.

Well if you introduce a keyword, it's easy

LET declaration IN expression

(let A : constant Integer := X * Y in A * A + (A - 1))

If you don't like introducing a keyword (which I think is a reasonable
reluctance, you could have an unreserved keyword (would work to have let be
unreserved), or use one of the following

     (A * A + (A - 1) with A : constant Integer := 23)

     (do A : constant Integer := 23 in ....)

     (use A : constant Integer := 23 in ....)

or just

     (A : constant Integer := 23 in ...)

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

From: Tucker Taft
Date: Saturday, May 1, 2010  1:42 PM

> ...
> or just
>
>     (A : constant Integer := 23 in ...)

Unfortunately membership test creates
a possible ambiguity here.

You could perhaps use "with...do" instead of "let ... in"

   (with A = <expression>, B = <expression>, ... do ...)

If these are all constants, I don't see the need for
": constant <type> :=" when "=" will do.

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

[Editor's note: There are another 120 messages in this thread; ran out of
time to get them filed. They'll appear soon...]