Version 1.1 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).

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