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

From: Randy Brukardt
Sent: Wednesday October 26, 2011  6:38 PM

John writes in his unfinished Rationale draft:

...
If several aspects are given to a procedure then we simply put them together
thus

procedure Kill
   with Inline, No_Return;

rather than having to supply several pragmas (which careless program maintenance
might have scattered around).

In the case of a procedure without a distinct specification, the aspect
specification goes in the procedure body before is thus

procedure Do_It( ... )
   with Inline is
   ...
begin
   ...
end Do_It;

...
In the case of an abstract subprogram and null subprogram which never have
bodies, the aspect specification goes after is abstract or is null thus

procedure Enqueue( ... ) is abstract
   with Synchronization => By_Entry;
procedure Nothing is null
   with Something;

--------------------

Am I the only one that sees something wrong with this picture?? The aspect
specification goes before the "is" for a body, and *after* the "is" for an
abstract or null subprogram??? I think that will be confusing for years to come,
given the minor difference between these.

John doesn't mention it, but an expression function is similar to a null
procedure:

function Inc (A : Integer) return Integer is (A + 1)
   with Inline;

which is bizarre when the equivalent body would be:

function Inc (A : Integer) return Integer
   with inline is
begin
   return A + 1;
end Inc;

I'd strongly suggest moving the aspect specification in front of the "is"
for abstract subprograms, expression functions, and null procedures. (Moving the
one for the normal body would not make sense, since it would remove it from the
specification of the subprogram.)

Note that we still wouldn't be 100% consistent, as generic instantiations have
it at the end (after the "is"). I'd suggest moving those as well before the
"is", as packages already have the specification before the "is".

-------------------

I think Brad may have made a similar suggestion back in the day, but we didn't
act on it beecause it seemed to make more sense to have the subprogram's aspects
after the "is". But that was before we added the subprogram body aspects, which
change the dynamic a lot.

Anyway, this is something that we have to decide now, because if we don't make a
change now, it will be forever too late to do so.

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

From: Tucker Taft
Sent: Wednesday October 26, 2011  10:04 PM

I vote for no change.

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

From: Robert Dewar
Sent: Wednesday October 26, 2011  10:14 PM

I agree with no change, it's awfully late for a syntactic change like this,
especially when the arguments in favor are by no means fully convincing.

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

From: Randy Brukardt
Sent: Wednesday October 26, 2011  10:44 PM

Well it would be better to be late with a change that would increase consistency
than to not do it at all and live forever with a mess.

If "make all subprograms have the same syntactic form vis-a-vis
aspect_specifications" is not "fully convincing", I find it hard to imagine any
argument about any syntax that would be convincing -- there is a certain amount
of taste involved. It's surely "fully convincing" for me! In virtually every
example I've ever written, I've always put the aspect_specification in front of
the "is". Having it afterwards for some, but not all, subprograms seems to me
like a continual source of errors. I can't imagine ever getting "used to" this
confusing syntax, because I don't think of "abstract subprogram" as something
syntactically different from other "normal" forms of subprogram.

One additional point: the current syntax buries the "is abstract" in the middle
of the text. I know I'm used to looking for it (and  "is" and ";") at the end of
the specification, right before the blank line. This syntax increases the
chances it will get missed.

There is an alternative, which is to drop the aspect_specification from
subprogram_bodies. I can imagine the rule for subprograms being put the
aspect_specification at the semicolon -- but there is no way to do that for a
subprogram_body. It's not worth the confusion to allow it on bodies if we're not
willing to change the other syntax (it's really only exists to allow tasking
programs to put a priority on the main subprogram without a separate
specification -- which always struck me as a weird way to do that in the first
place.)

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

From: Tucker Taft
Sent: Wednesday October 26, 2011  11:16 PM

A general rule could be that the aspect specification goes at the final ";"
except for program units that can have nested declarations with their own aspect
specifications, in which case it goes immediately after the "is".

Or something like that...

I find it much preferable to keep the "is abstract" and "is null" immediately
next to the subprogram declaration, and follow the whole thing with an aspect
specification, than to have a dangling "is null;" or "is abstract;" after a
long-winded aspect specification.

For bodies, before the "is" makes sense, because you are about to launch off
into a bunch of nested declarations.

I don't think of "is null;" or "is abstract;" as being like a proper body, but
rather as more like a spec.  It is true that these things obviate the need for a
body, but I don't think of them as *being* bodies at all.

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

From: Tucker Taft
Sent: Wednesday October 26, 2011  11:17 PM

In other words, I think we got it right with the current rules, and don't agree
with your argument for consistency between bodies and null/abstract subprogram
declarations.

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

From: Robert Dewar
Sent: Wednesday October 26, 2011  11:37 PM

I 100% agree with Tuck's reasoning and conclusions here

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

From: Randy Brukardt
Sent: Wednesday October 26, 2011  11:53 PM

> A general rule could be that the aspect specification goes at the
> final ";" except for program units that can have nested declarations
> with their own aspect specifications, in which case it goes
> immediately after the "is".

Fine, except that it seems to lead to nonsense results.

...
> I don't think of "is null;" or "is abstract;" as being like a proper
> body, but rather as more like a spec.  It is true that these things
> obviate the need for a body, but I don't think of them as *being*
> bodies at all.

I think you are missing my point (I must not be making it well). This is not
about specs or bodies, it's about the common part that all subprograms have. The
current syntax seems confused as to whether the aspect_specification belongs to
that common part. Given that (almost) all forms of subprogram have aspect
specifications, it seems weird to not consider it part of the common part. And
that means that the aspect specification belongs before the parts that differ
(i.e., before the "is" in all forms).

Unless I'm in language-lawyer mode, I almost never think about subprogram
specifications, bodies, abstract subprograms, null procedures, and expression
functions as being different things -- they're the same thing with different
options. As such I expect maximum commonality in syntax. We seem to be getting
away from that principle -- and for not very convincing reasons -- and that's
what bothers me.

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

From: Tucker Taft
Sent: Thursday October 27, 2011  12:13 AM

I perceive the "is" for a subprogram body as quite different from the "is" for
instantiations, null procedures, and abstract subprograms (with apologies to
Bill Clinton ;-). The former "is" is more like a separator between the
specification and the code.  The latter "is"es are more being used to specify
equivalences.

I agree this is a matter of perception, but you seem to be claiming your point
of view is obviously correct, but apparently it is not to some of us.  I also
vaguely remember discussing this issue and settling on the current syntax, and I
don't see a compelling reason to re-open this discussion.

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  1:00 AM

> I perceive the "is" for a subprogram body as quite different from the
> "is" for instantiations, null procedures, and abstract subprograms
> (with apologies to Bill Clinton ;-).
> The former "is" is more like a separator between the specification and
> the code.  The latter "is"es are more being used to specify
> equivalences.

I think we could make an argument that "is abstract" is not the best syntax, but
we're kind of stuck with it.

> I agree this is a matter of perception, but you seem to be claiming
> your point of view is obviously correct, but apparently it is not to
> some of us.

I'm sorry if you got that impression; it wasn't my intent. It's obviously
correct *to me*, and I'm trying to explain what I see and feel and think many
other Ada programmers will also feel.

But it seems you are continuing to ignore my primary point: is an
aspect_specification part of the "common part" of a subprogram or not? In my
view, it is a first-class part of the "common part" of a subprogram (I hesitate
to call that part the "specification", because if I do, people will start
talking about how bodies are different, which is irrelevant -- every body
includes a specification syntactically, and I'm talking syntactically not
semantically), and as such it should be treated the same in all subprograms.
There is certainly room to have a difference of opinion on this point, and I've
been waiting for someone to make an argument that it is not part of the "common
part", but I haven't heard any such argument.

But if someone can't make a sane argument for why it is not part of the "common
part" of a subprogram (the subprogram specification), then it follows that the
syntax should be the same for all subprograms. (And that it should be allowed on
stubs, too - another issue which bothers me, although not to the same level
because hardly anyone uses stubs.)

> I also vaguely remember
> discussing this issue and settling on the current syntax, and I don't
> see a compelling reason to re-open this discussion.

We discussed this in the context of generic instantiations. At the time, we
didn't have aspects on subprogram bodies, so while I wasn't thrilled by the
syntax, I could live with it because it was consistent (the aspect_specification
always went at the end with the semicolon for subprograms). [I really didn't
like the inconsistency with packages, but there didn't seem to be a way to make
them consistent.] But now subprograms are no longer consistent, and that changes
the level of the concern for me. And admittedly, I hadn't seen just how silly it
looks until John laid it out in his draft.

Hopefully someone else will speak up here, because if I am way off base I'd like
to know why.

This is an issue that *has* be resolved in my mind before I can support
progressing the Standard (mainly because once the Standard goes forward we are
stuck with this syntax forever). While virtually anything else can be fixed
after the fact if need be, there is no chance to do so here. (I suspect that
Robert would claim it is already too late, given that a widely used
implementation already exists. But such an implementation is by definition
unofficial and subject to change -- if not, we aren't even needed because that
implementation IS the standard.)

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

From: Jean-Pierre Rosen
Sent: Thursday October 27, 2011  2:28 AM

I'm rather siding with Randy here, especially from the point of view of
teaching: uniformity is much simpler to explain.

...
> I agree with no change, it's awfully late for a syntactic change like
> this, especially when the arguments in favor are by no means fully
> convincing.

Here is (maybe) one: don't forget that the ARG doesn't have the final word, but
ISO. If some NB dislikes the current syntax, we can get comments at the ISO
level.

I think a non-uniform syntax could trigger comments; a uniform one won't. If a
change has to be made, I think we are much better off making it now than later.

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

From: Bob Duff
Sent: Thursday October 27, 2011  4:10 AM

> I'd strongly suggest moving the aspect specification in front of the "is"
> for abstract subprograms, expression functions, and null procedures.

I could go either way.  Therefore, I vote to keep it as is.

I see Randy's consistency point, but there's also consistency with
instantiations, and with packages.  Procedure bodies and package specs are
"big", so you don't want aspects at the end. Abstract procedures are small, so
aspects go at the end, like other small things.

> Anyway, this is something that we have to decide now, because if we
> don't make a change now, it will be forever too late to do so.

Yes.  That doesn't frighten me -- the syntax is imperfect, but tolerable.  The
only way to do better would be to redesign the syntax from scratch, with aspects
in mind.

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

From: Bob Duff
Sent: Thursday October 27, 2011  4:13 AM

>...(And that it
> should be allowed on stubs, too - another issue which bothers me, ...

That seems like a real problem.  If you have No_Return on a subunit body, but
not on the stub, how is the compiler supposed to know about it at call sites?

It's only an issue for compilers that do "true" separate compilation of
subunits.

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

From: Jean-Pierre Rosen
Sent: Thursday October 27, 2011  6:51 AM

>> ...(And that it
>> should be allowed on stubs, too - another issue which bothers me, ...
>
> That seems like a real problem.  If you have No_Return on a subunit
> body, but not on the stub, how is the compiler supposed to know about
> it at call sites?

I'd say allow aspects on stubs and not on proper bodies.

I see proper bodies just like a convenience to put the body in a separate file.
The real body declaration is the stub.

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

From: Tucker Taft
Sent: Thursday October 27, 2011  7:32 AM

Generic instantiations need to fit into this.

    procedure Conv is new Ada.Unchecked_Deallocation(Obj, Ptr)
      with Inline;

is more readable to me than

    procedure Free with Inline is new Ada.Unchecked_Deallocation(Obj, Ptr);

I think aspect specifications are *not* part of the "common part" of a
subprogram declaration, but are rather to be "tacked onto the end" which is the
general rule for them on declarations.  Bodies and packages require the aspect
specification earlier so it can appear before all of the nested declarations.

I think this is also better for transition, because some projects probably
already have formatting rules for things like generic instantiations, and
putting something at the end is pretty easy, whereas fitting some piece of
syntax of arbitrary length in to the middle of a construct like generic
instantiation adds to the burden of started to use it on a project.

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

From: Edmond Schonberg
Sent: Thursday October 27, 2011  7:41 AM

> For bodies, before the "is" makes sense, because you are about to
> launch off into a bunch of nested declarations.
>
> I don't think of "is null;" or "is abstract;" as being like a proper
> body, but rather as more like a spec.  It is true that these things
> obviate the need for a body, but I don't think of them as *being*
> bodies at all.

I agree with this point of view.  For subprogram declarations I find that it
reads better to have the aspects right before the semicolon. A minor point is
that to decorate existing software with new aspects it will feel easier to go to
the end of the declaration and open a new line with "with" than inserting it in
the middle.

I expect that aspects on subprogram bodies with be rarer (of course we have to
live with bodies without specs, which to my mind is a 30-year wart). In any case
it makes sense that the syntax for bodies would be different,  Concerning stubs,
I would favor leaving aspects out, and requiring the presence of a previous spec
if aspects are needed.

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

From: John Barnes
Sent: Thursday October 27, 2011  8:11 AM

> John doesn't mention it, but an expression function is similar to a
> null procedure:

John didn't mention it because at that point he hadn't introduced them (but he
will add such an example)

> function Inc (A : Integer) return Integer is (A + 1)
>   with Inline;
>
> which is bizarre when the equivalent body would be:
>
> function Inc (A : Integer) return Integer
>   with inline is
> begin
>   return A + 1;
> end Inc;

I do agree that is perhaps odd. I could certainly vote for moving that one.

But I think it rather depends upon physically how big the expression is and how
big the aspect is.

However, the ones I trip up on are tasks and tiny packages.
Tasks are odd because they might or might not have an "is". They could be just

task T;

or

task T is
   entry E ...
end T;

If you read the Intro now published in AUJ you will find I made a mistake on
page 175 by writing both

taks My_Task is
   with CPU => 10;

and later

task My_Task
   with Dispatching_Domain => My_Domain;

No one noticed this and when I circulated a draft of the next bit of the
rational to Tuck and Randy, they didn't spot that I kept on doing this.

This is probably why I dislike

package Ada
   with Pure is
end Ada;

(I just hate "end is"!)

as opposed to

package Ada is
   pragma Pure;
end Ada;

Anyway, I can live with it. (But I still really really hate subtype
predicates.)

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

From: Bob Duff
Sent: Thursday October 27, 2011  8:30 AM

> Anyway, I can live with it. (But I still really really hate subtype
> predicates.)

And subtype predicates are my favorite new feature of Ada 2012!

I hope we can remain friends, despite this difference of opinion.  ;-)

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

From: Robert Dewar
Sent: Thursday October 27, 2011  9:38 AM

For me, Randy's emphasis on attempted simpler rules and more uniformity in the
syntax are about making the language easier to write. Similarly JPR's concerns
are about making it easier to teach how to write.

But that's always a secondary concern, readability is the most important
concern, and uniformity is not so important there, after all you read the code
and the aspects are read wherever they are.

   procedure X is abstract;

is indeed not an ideal syntax, probably

   abstract procedure X;

would have been better, but too late now, and the first form above is not really
that different, and importantly the aspect keyword occurs right at the start.

But if we let the aspects come between procedure and abstract we are seriously
damaging the readability. It is important to know right up front that you are
dealing with an abstract procedure, and that choice would damage this important
factor in readability.

To me, the existing rules are the best balance for good readability.

I find Randy's suggested changes not just unnecessary, but actively harmful. I
understqand the uniformity argument, but I agree with Tuck, the function of the
keyword IS varies considerably in terms of readability, and trying to make the
aspect rules consistent with respect to this keyword is a mistake.

I really see no new information here that would justify revisiting the original
decisions.

There are a number of things I don't like in the Ada 2012 decisions, but that
doesa not mean I am about to raise them at this point, since I consider they
have been properly discussed and decided, my individual discomfort with a
previously made decision is not a reason to reopen the discussion.

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

From: Robert Dewar
Sent: Thursday October 27, 2011  9:40 AM

> I expect that aspects on subprogram bodies with be rarer (of course we
> have to live with bodies without specs, which to my mind is a 30-year
> wart). In any case it makes sense that the syntax for bodies would be different,  Concerning stubs, I would favor leaving aspects out, and requiring the presence of a previous spec if aspects are needed.

I prefer to allow user defined aspects on all declarations, who knows what they
may be used for, and it is a pity to force an implementation to come up with an
impl-defined pragma when an impl-defined aspect would be neater.

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

From: Robert Dewar
Sent: Thursday October 27, 2011  9:43 AM

>> Anyway, I can live with it. (But I still really really hate subtype
>> predicates.)
>
> And subtype predicates are my favorite new feature of Ada 2012!

Me too (favorite new feature), although I disklike the official names, luckily
my favorite implementation allows me to use what to me is the proper name,
Predicate, instead of the peculiar names that the standard insists on :-)

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

From: Erhard Ploedereder
Sent: Thursday October 27, 2011  12:46 PM

> I'd say allow aspects on stubs and not on proper bodies.

I support this (until someone tells me that they need them on bodies for sure,
because ....).

(It would also save us any number of discussions about  distinguishing
"spec-ish" from "impl-ish" aspects.)

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

From: Brad Moore
Sent: Thursday October 27, 2011  8:13 AM

> I see Randy's consistency point, but there's also consistency with
> instantiations, and with packages.

I have to admit I am siding with Randy's point of view.
For subprograms, it seems simpler and tidier to say;

Anything after the "is" is about the implementation, whether its a null
procedure, an abstract procedure, or a real body.

Anything before the "is", is specification. Aspects (in particular, Pre and
Post) should be part of the specification. Subprogram aspects are tacked on at
the end of the specification.

To me this is still consistent with the current syntax for instantiations and
packages. For packages, the entire text of the package *is* the specification,
so the aspect occurs in the specification, regardless whether it occurs before
or after the "is", and for instantiations, the implementation is in the generic
body, while the aspect can be viewed as being in the specification along with
the instantiation, so I think it's OK for the aspects to follow the "is" in this
case.

I also don't find the argument about having "is null" at the end getting lost by
the reader that compelling. Some indentation can make this stand out.

 procedure Some_Procedure
      (Some_Parameter : Integer;
       Another_Parameter : Integer;
       Yet_Another_Parameter : Integer)
    with Pre => Something,
         Post => Something_else,
         Some_Other_Aspect => Something_Different
 is abstract;

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

From: Robert Dewar
Sent: Thursday October 27, 2011  1:43 PM

But that's a completely different style of procedure spec than many are used to,
and one would have to change all of them for consistency, so that seems a big
disadvantage to me.

You want to make it easy to add aspects to existing programs, otherwise people
will just forget about the aspects and use the corresponding pragmas.

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

From: Bob Duff
Sent: Thursday October 27, 2011  2:01 PM

> Anything after the "is" is about the implementation, whether its a
> null procedure, an abstract procedure, or a real body.

I don't see how "abstract" can be considered implementation.
It appears in the visible part of the package, and there are all sorts of
legality rules that require this information to be visible to clients.  Same
with "null".

If "abstract" were an implementation detail, then it would be part of the
subprogram body, hidden in the package body.

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

From: Bob Duff
Sent: Thursday October 27, 2011  2:53 PM

> This is an issue that *has* be resolved in my mind before I can
> support progressing the Standard (mainly because once the Standard
> goes forward we are stuck with this syntax forever).

Yes, if we keep the syntax, or change it, whatever we decide we will be stuck
with forever.  But either way, it's not that big of a deal.

>...While virtually anything else can be  fixed after the fact if need
>be, ...

Heh?  Hardly anything can be fixed after the fact, because of compatibility.

That's why we still have the idiotic syntax "task type T is...", instead of the
more consistent "type T is task...".

And it's why we still have all those pragmas, even though many people think
aspects are better.

And I can think of hundreds of other design flaws (mostly
minor) that we've been stuck with since 83, 95, and 2005.

>...there is no chance to do so here. (I  suspect that Robert would
>claim it is already too late, given that a widely  used implementation
>already exists.

I don't think Robert would claim that.  I certainly wouldn't.
GNAT has implemented almost all of Ada 2012 (not quite all), but users have been
warned that the implementation might need to change if the language changes.
(Hopefully, there won't be any major or gratuitous changes at this point.)

Also, I think your "widely used" above is not correct -- most folks are
conservatively sticking with Ada 95 or Ada 2005 (or even Ada 83 in some cases).
Only the adventurous use Ada 2012.

> ...But such an implementation is by
> definition unofficial and subject to change -- if not, we aren't even
> needed because that implementation IS the standard.)

Agreed.

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

From: Robert Dewar
Sent: Thursday October 27, 2011  3:12 PM

> And it's why we still have all those pragmas, even though many people
> think aspects are better.

One reason I often prefer the pragmas is that somethings more logically often
belong in the private part since they are not a concern of the client (size of
types, layout of types, inlining of subprograms etc).

> I don't think Robert would claim that.  I certainly wouldn't.
> GNAT has implemented almost all of Ada 2012 (not quite all), but users
> have been warned that the implementation might need to change if the
> language changes.  (Hopefully, there won't be any major or gratuitous
> changes at this point.)

My objects to Randy's changes are not at all based on concern for the current
implementation, but rather a feeling that far from being improvments, they are
activelg undesirable.

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

From: Tucker Taft
Sent: Thursday October 27, 2011  4:14 PM

> I'd say allow aspects on stubs and not on proper bodies.

I presume what you mean is: "allow them on stubs, but disallow them on proper
bodies that are *subunits*."

"Proper body" in general refers to any subprogram body, whether or not it has a
separate stub.

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

From: Stephen Michell
Sent: Thursday October 27, 2011  4:13 PM

>> I expect that aspects on subprogram bodies with be rarer (of course
>> we have to live with bodies without specs, which to my mind is a
>> 30-year wart). In any case it makes sense that the syntax for bodies would
>> be different,  Concerning stubs, I would favor leaving aspects out, and
>> requiring the presence of a previous spec if aspects are needed.
>
> I prefer to allow user defined aspects on all declarations, who knows
> what they may be used for, and it is a pity to force an implementation
> to come up with an impl-defined pragma when an impl-defined aspect would
> be neater.

You will find that there are many predicates on subprogram bodies. The body
implements the spec and you often need to restate predicates in terms of the
implementation, with package state and other subprogram predicates (usually
function results). It is necessary to separate the implementation from the
specification.

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

From: Edmond Schonberg
Sent: Thursday October 27, 2011  4:20 PM

But the language doesn't let you do that:  the current rule is that you can give
aspects on bodies only if they are spec-less  (13.3.1):

35/3 An aspect shall not be specified in an aspect_specification given on a
     subprogram_body that is a completion of another declaration.

So we have a disconnect if you think you will need both.

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

From: Robert Dewar
Sent: Thursday October 27, 2011  5:27 PM

> You will find that there are many predicates on subprogram bodies.
> The body implements the spec and you often need to restate predicates
> in terms of the implementation, with package state and other
> subprogram predicates (usually function results). It is necessary to
> separate the implementation from the specification.

While this may be true (and indeed in GNAT precondition and postcondition
pragmas are allowed in subprogram bodies), it is my understanding that the pre
and post aspects can only apply to a subprogram declaration, and not to the
body.

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  7:14 PM

> Generic instantiations need to fit into this.
>
>     procedure Conv is new Ada.Unchecked_Deallocation(Obj, Ptr)
>       with Inline;
>
> is more readable to me than
>
>     procedure Free with Inline is new Ada.Unchecked_Deallocation(Obj, Ptr);

Sure, but that's not how you'd format it:

      procedure Free
         with Inline
         is new Ada.Unchecked_Deallocation(Obj, Ptr);

I already format most instantations on multiple lines (they're too long to put
on one line), so this isn't a big change in practice.

(BTW, I've been purposely avoiding reading this thread until now, so that I
didn't monoplize the conversation. Time to catch up now.)

> I think aspect specifications are *not* part of the "common part" of a
> subprogram declaration, but are rather to be "tacked onto the end"
> which is the general rule for them on declarations.  Bodies and
> packages require the aspect specification earlier so it can appear
> before all of the nested declarations.

But why should they be tacked on to the end? They form part of the formal
contract for a subprogram (at least Pre, Post, No_Return,  and Synchronization)
-- it's not at all clear that they should be separated from the specification.

> I think this is also better for transition, because some projects
> probably already have formatting rules for things like generic
> instantiations, and putting something at the end is pretty easy,
> whereas fitting some piece of syntax of arbitrary length in to the
> middle of a construct like generic instantiation adds to the burden of
> started to use it on a project.

I think Robert said something similar in another message. I agree this is an
interesting point, but it seems to go against your typical philosophy that we
shouldn't have features that look "bolted on". Here you seem to be advocating
that this feature should look "bolted on".

Aside: No matter what rule we adopt, we need a simple explanation of it, and
John should have that explanation in the Rationale. It shouldn't be necessary to
think of it as a hodge-podge...

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  7:22 PM

...
> There are a number of things I don't like in the Ada 2012 decisions,
> but that doesa not mean I am about to raise them at this point, since
> I consider they have been properly discussed and decided, my
> individual discomfort with a previously made decision is not a reason
> to reopen the discussion.

The problem here is that we never really decided this topic. This syntax just
happened, and in previous discussions it's been clear that there is a lot of
discomfort with this syntax. We've never had a enough of a consensus to make a
change, so essentially we stuck with the status quo. But that isn't necessarily
the best way to design new syntax -- I'd be a lot happier if it was clear that
almost everyone *liked* this syntax. With a few exceptions, however, all we seem
to have is reactions from grudging acceptance to downright hostility.

We had that effect in Ada 2005 with coextensions, and I now realize that going
forward with those above all of the objections was a serious mistake. (It gives
me a lot more standards work than I'd otherwise have, but I'd say that's the
only positive of the concept.:-) And there's probably a better use of the ARA's
money...)

Perhaps there really is nothing better, but I'd rather explore that while we
still have a chance rather than waiting until we have serious regrets years from
now.

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  7:31 PM

> > This is an issue that *has* be resolved in my mind before I can
> > support progressing the Standard (mainly because once the Standard
> > goes forward we are stuck with this syntax forever).
>
> Yes, if we keep the syntax, or change it, whatever we decide we will
> be stuck with forever.  But either way, it's not that big of a deal.
>
> >...While virtually anything else can be  fixed after the fact if need
> >be, ...
>
> Heh?  Hardly anything can be fixed after the fact, because of
> compatibility.

I was thinking of changes that happen relatively soon. For those, semantics
changes only take a BI, and we don't consider compatibility (assuming it has to
do with a new feature). We're always looser with these changes right after a new
standard, because of the need to fix unintended features. (Such as the one that
in Ada 2005 would have required keeping extra "constrained" bits in access
values.)

You're right in the long run, although we can be pretty clever about keeping
compatibility. But I don't recall *ever* having done an incompatible syntax
change (thinking of new reserved words as a lexical change).

> That's why we still have the idiotic syntax "task type T is...",
> instead of the more consistent "type T is task...".

That's syntax. It never, ever changes -- it just gets extended.

> And it's why we still have all those pragmas, even though many people
> think aspects are better.

Arguably, that's syntax as well.

> And I can think of hundreds of other design flaws (mostly
> minor) that we've been stuck with since 83, 95, and 2005.

Hundreds seems like an over-estimate to me, while I wouldn't disagree that some
exist.

But we do tend to be more flexible in removing non-syntax design flaws. For
instance, we decided to make all record types compose. I can't imagine a
circumstance where we would change the syntax for task types (to use your
example).

That's why I consider getting the syntax right a higher priority than getting
the semantics right (even if that seems backwards).

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

From: Robert Dewar
Sent: Thursday October 27, 2011  8:28 PM

> Aside: No matter what rule we adopt, we need a simple explanation of
> it, and John should have that explanation in the Rationale. It
> shouldn't be necessary to think of it as a hodge-podge...

Well syntax rules are in the syntax, and I see no reason to think you need much
of an explanation beyond the easily read syntax rules.

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  8:51 PM

> > Aside: No matter what rule we adopt, we need a simple explanation of
> > it, and John should have that explanation in the Rationale. It
> > shouldn't be necessary to think of it as a hodge-podge...
>
> Well syntax rules are in the syntax, and I see no reason to think you
> need much of an explanation beyond the easily read syntax rules.

I think it would be highly helpful if there was some relatively simple rule to
explain the syntax; that's kinda the point of a Rationale, after all.

Something like: "The aspect_specification goes at the end of a declaration,
unless that declaration is "large", in which case it goes at some randomly
determined point." ;-)

(Tucker had a more serious suggestion earlier, except that I don't think it was
right as a subprogram specification is a kind of program unit, and his rule
tried to treat program units specially.)

So long as there is a reasonably explainable rule for the syntax, I will be
reasonably placated. (It will also help when determining where
aspect_specification should go in future syntax.)

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

From: Robert Dewar
Sent: Thursday October 27, 2011  8:57 PM

> I think it would be highly helpful if there was some relatively simple
> rule to explain the syntax; that's kinda the point of a Rationale, after all.

The rationale is that the appects go where they make sense. Yes, a simple rule
is nice, but not if the simple rule leads to ugly to read constructions.

> (Tucker had a more serious suggestion earlier, except that I don't
> think it was right as a subprogram specification is a kind of program
> unit, and his rule tried to treat program units specially.)

I see no reason not to treat them specially in this context

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

From: Robert Dewar
Sent: Thursday October 27, 2011  8:32 PM

> You're right in the long run, although we can be pretty clever about
> keeping compatibility. But I don't recall *ever* having done an
> incompatible syntax change (thinking of new reserved words as a lexical change).

Sure we have, one example: simple expressions as case alternatives in Ada 2012,
this bit someone using GNAT just the other day.

>> That's why we still have the idiotic syntax "task type T is...",
>> instead of the more consistent "type T is task...".

I don't think anything is iodiotic about task type T (and I still think it is
too bad we did not end up with class type T ...)

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

From: Stephen Michell
Sent: Thursday October 27, 2011  8:42 PM

In response to Ed's feedback about pre and post conditions on subprogram bodies.

So here is an example of why it is needed. This is a single package from a small
game that I used in doing formal proof examples. The game is Gobble or Greedy. I
think that everyone knows it. You choose a number of candies or marbles or
something. You can take between 1 to N at a time (here N is 5). The person that
takes the last one loses.

The proof system here was Spark. In the sake of simplicity, I am going to
dramatically shorten it. Consider 1 package Play_Game. This contains the
following procedures
   Player_Move  -- called once each time the human player's input is needed

   Best_Move  -- evaluates the best move to win

   Play_Game  -- iterates calling Plater_Move & Best_Move until the termination conditions are met.

I'll make comments at the end.

Here is the spec  (leaving out many of the Spark-isms to concentrate on the
preconditions and postconditions)

with Support;
use type Support.Player_Choices;
with Gobble_Io;
package Play
is

 --# type State_Type is Abstract;

 --- Proof function
 --# function Winning_Position(state: State_Type) return Boolean;
 -- True any time tokens_left = 1 mod (min+max).

 --# function Tokens_LeftS(state: State_Type ) return Support.Selection_Range;

 --# function Player_First_Move(State: State_Type) return Support.Selection_Range;

 --------------------------------------------------
 --
 --  player_move
 --
 --------------------------------------------------
 --
 procedure Player_Move ( Move : out Support.Selection_Range ) ;
 --# post   winning_position(state~) -> not winning_position(state);

 procedure best_move( player        : in     Support.Player_Choices;
                      our_best_move :    out Support.Selection_Range;
                      who_won       :    out Support.Player_Choices ) ;
 --# global state;
 --# derives our_best_move from  state          &
 --#         who_won       from  state, player;
 --# pre   (Tokens_LeftS(state) > Support.Minimum_Selection and
 --#       (player = support.machine));
 --# post (( Tokens_LeftS(state)  mod (support.minimum_selection+support.maximum_selection) = 1)
 --#        -> (    our_best_move = support.minimum_selection
 --#            and who_won = support.human))
 --#      and
 --#      ((tokens_leftS(state) mod (support.minimum_selection+support.maximum_selection) = 0)
 --#        -> (    who_won       = support.machine
 --#            and our_best_move = Support.Maximum_Selection))
 --#      and
 --#       (( tokens_leftS(state) mod (support.minimum_selection+support.maximum_selection)
 --#         in (support.minimum_selection+1)..Support.Maximum_selection )
 --#        -> (     who_won = support.machine
 --#            and  our_best_move = ( Tokens_LeftS(State) mod
 --#                                   (support.minimum_selection+support.maximum_selection)
 --#                                  - support.Minimum_Selection)));

 procedure play_game( my_goal : in Support.Starting_Token_Range;
                      Who_Won : out Support.Player_Choices ) ;  --# global state, gobble_io.state;
 --# derives who_won         from my_goal, state, gobble_io.state &
 --#         state           from my_goal, state, gobble_io.state &
 --#         gobble_io.state from          state, gobble_io.state;
 --# post     ((my_goal mod (support.minimum_selection+support.maximum_selection)
 --#           = support.minimum_selection) -> who_won = support.machine)
 --#      and ((   (my_goal mod (support.minimum_selection+support.maximum_selection)
 --#              /= support.minimum_selection)
 --#           and Player_First_Move(State) mod ( support.minimum_selection
 --#                                                           +support.maximum_selection)
 --#               = My_Goal - support.minimum_selection)
 --#          -> who_won = support.machine);

 end Play;

Now here is the body

Package body Play
--# own State  is Starting_Tokens, Tokens_Left, First_Move; is

 Starting_Tokens : Support.Starting_Token_Range;
 Tokens_Left     : Support.Token_Range;
 First_Move      : Support.Selection_Range ;

 -- factor is the part that governs winning - the only winning position is 1 mod factor
 Factor          : constant :=  Support.Minimum_Selection+Support.Maximum_Selection;

 --------------------------------------------------
 --
 --  player_move
 --
 --------------------------------------------------
 --
 procedure Player_Move ( move : out Support.Selection_Range )
   --# pre         Tokens_Left     in Support.Token_Range and
   --#             Starting_Tokens in Support.Token_Range;
   --# post        move < tokens_Left~                and
   --#             move in Support.Selection_Range    and
   --#             Tokens_Left = Tokens_Left~ - Move;
 is

    valid_choice   : boolean;
    Humans_Choice  : Integer;
    begin
       valid_choice  := false;
       Humans_Choice := 0;

       while (not Valid_Choice) loop
          --# assert not (    (Humans_Choice in Support.Selection_Range)
          --#             and Humans_Choice < Tokens_Left)
          --#        and tokens_left = tokens_left~;
          Gobble_Io.Request_move;
          Gobble_Io.Get_Choice(Humans_Choice);

          valid_choice := (    (Humans_Choice in Support.Selection_Range)
                           and Humans_Choice < Tokens_Left);
       end loop;

       Move        := Humans_Choice;
       Tokens_Left := Tokens_Left-Move;

    end player_move;


--------------------------------------------------
--
--  best_move
--
-- This subprogram figures out the best possible move
-- for "player". It does this by playing all possible
-- moves available to it and evaluating each move.
-- The secret is in the move evaluation.
-- Moves are evaluated by calling "best_move" for
-- the opponent. If best_move(...opponent...) tells
-- us that we won, then the move that we just selected
-- is a winner.
--
--------------------------------------------------
--

   procedure best_move( -- total         : in     integer;
                        -- my_goal          : in     integer;
                        player        : in     Support.Player_Choices;
                        our_best_move :    out Support.Selection_Range;
                        who_won       :    out Support.Player_Choices )

   --# pre   (Tokens_Left > support.minimum_selection) and
   --#       (player = support.machine);

   --# post     Our_Best_Move in Support.Selection_Range
   --#      and (   (     Who_Won = Support.Machine
   --#                and Tokens_Left mod Factor =0
   --#                and Our_Best_Move = support.maximum_selection)
   --#           or (    Who_Won = Support.Machine
   --#               and Tokens_Left mod Factor in 2..5
   --#               and our_best_move = (Tokens_Left mod Factor - support.minimum_selection))
   --#           or (    Who_Won = Support.Human
   --#               and Tokens_Left mod Factor = 1
   --#               and our_best_move = support.minimum_selection));

   is
      Desired_Move : Integer;

   begin
      Desired_Move := Tokens_Left mod Factor;

      if Desired_Move = Support.Minimum_Selection  then
         Our_Best_Move := Support.Minimum_Selection ;
         Who_won       := Support.Other_Player(Player);
      elsif Desired_Move = 0 then
         Our_Best_Move := Support.Maximum_Selection;
         Who_Won       := Player;
      else
         Our_Best_Move := Desired_Move - Support.Minimum_Selection;
         Who_Won       := Player;
      end if;
   end Best_Move;

--------------------------------------------------
--
--  play_game
--
-- This is the routine that plays a game. Each time
-- around the loop it gets a player move and calculates
-- its own move. It figures out it's best move by
-- calling the subprogram best_move.
--
--------------------------------------------------

 procedure play_game(My_Goal : in Support.Starting_Token_Range;
                     who_won :    out  Support.Player_Choices )
 --# Global Tokens_Left, Starting_Tokens, First_Move, Gobble_IO.State;
 --
 --# post     (Starting_Tokens mod (Factor) = support.minimum_selection
 --#           -> who_won = support.machine)
 --#      and ((   Starting_Tokens mod (Factor)  /= support.minimum_selection
 --#           and (Starting_Tokens-First_Move mod Factor = support.minimum_selection))
 --#          -> who_won = support.machine);

 is

    Done         : Boolean;
    Move         : Support.Selection_Range;
    Players_Move : Support.Selection_Range;
    Winning      : Support.Player_Choices;

 begin
    Starting_Tokens := My_Goal;
    Tokens_Left     := My_Goal;
    Player_Move ( Players_Move);  -- updates Tokens_Left
    First_Move := Players_Move;
    Done := False;

    best_move( Support.machine, move, Winning );
    Gobble_Io.report_move( move, Tokens_Left );
    Tokens_Left := Tokens_Left - Move; -- this is the actual machine move
    if Tokens_Left mod Factor = support.Minimum_Selection        then
       Winning := Support.Machine;
    end if;


    while not Done loop
       --# assert ((winning=support.machine) <->
       --#             (Tokens_Left mod Factor = support.Minimum_Selection)) and
       --#        (Winning=support.human <->
       --#             (Tokens_Left mod Factor /= support.Minimum_Selection))
       --#        and First_Move in    Support.Selection_Range
       --#        and not done;


       Player_Move ( Players_Move);  -- updates Tokens_Left
       Done := Support.winner( Tokens_Left);
       if Done then
          Winning := Support.Human;
       else
          best_move( Support.machine, move, Winning );
          Gobble_Io.report_move( move, Tokens_Left );
          Tokens_Left := Tokens_Left - Move; -- this is the actual machine move
          Done := Support.winner(Tokens_Left);
       end if;

    end loop;
    Who_Won := Winning;

  end Play_Game ;

end Play;


So hopefully you will notice:
We had state in the package body that are key to doing the proofs. These are
      Starting_Tokens : Support.Starting_Token_Range;
      Tokens_Left     : Support.Token_Range;
      First_Move      : Support.Selection_Range ; and
      Factor          : constant :=  Support.Minimum_Selection+Support.Maximum_Selection;
here.
They must be in the body, because if they are in the spec (even in a package
private) they can be updated from elsewhere and we cannot prove anything about
them.

So, In the spec we needed to create proof functions to carry the effects of the
state. Hence you will note the  proof function Player_First_Move, which in
Spark(S:State) return Selection_Range. In Spark you develop a formula to connect
it to the package variable First_Move. Then you prove that postcondition(body)
=> postcondition(spec).

The other proof functions have similar effects.

So what you need to do is prove
   pre(spec) & initial_body_state => pre(body)
  pre(body) && code(body) => post(body)
 post(body)  => final_Body_State & post(spec)

I would claim, therefore, that if we do not have preconditions and
postconditions on subprogram bodies, then they are not much use.

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

From: Robert Dewar
Sent: Thursday October 27, 2011  8:55 PM

> I would claim, therefore, that if we do not have preconditions and
> postconditions on subprogram bodies, then they are not much use.

I think that's far too strong.

The main purpose of pre and post conditions is to make a contract between the
caller and the callee, and for this they have to be in the spec obviously.

Pre and postconditions associated with the body are really nothing more than a
more convenient syntax for assertions.

Anyway, I think it is FAR too late to make any change here.
Note that in fact as I mentioned GNAT does allow precondition and postcondition
pragmas in the body.

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  9:05 PM

...
> I would claim, therefore, that if we do not have preconditions and
> postconditions on subprogram bodies, then they are not much use.

Remember that nothing in Ada 2012 is (directly) intended to support static
proofs (although they can be valuable aids for proofs). What the WG 9 resolution
asked us to do was to strenghten contracts, and preconditions and postconditions
in Ada 2012 are a contract element, just like constraints. In particular, a
precondition is an obligation on the caller of a routine, and postcondition is a
promise to the caller of the routine. Private contracts are pointless; I'd even
say that a private precondition is harmful: how can a caller meet an obligation
that it does not know about? Similarly, a promise that the caller does not know
about or understand is not of much value.

Thus, pre and post aren't allowed on bodies. If checks are needed in the body
that aren't known to the caller, we have pragma Assert for that purpose. (In
addition, it's often possible to add abstractions to use in the pre and post
conditions. Those needn't add much cost if they are modeled as expression
functions or otherwise inlined.)

Since the syntax of aspect_specifications are allowed on subprogram bodies, an
implementation-defined aspect could be allowed there -- but there are no
language-defined ones that are allowed on bodies that do have specifications.

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

From: Stephen Michell
Sent: Thursday October 27, 2011  9:13 PM

I agree that the contract is one of the reasons. The other reason is to prove
that the body implements the specification and satisfies the postcondition if
the precondition is true. Of course you need to have something akin to Spark's
proof functions to make it all work. You can do it in Ada with real functions,
but the argument will be that real functions require execution time resources,
at additional time cost and complexity.

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  9:41 PM

> I agree that the contract is one of the reasons. The other reason is
> ...

Sorry, there is no other reason. Pre and post conditions in Ada 2012 are purely
contract features. Any resemblance to any other feature, living or dead :-), is
purely coincidental.

Indeed, I would argue that using a contract feature for reasons unrelated to
contracts is likely to be confusing and maybe even harmful. I understand the
need for proof features, but these should not get mixed with contracts. It's
important (if proof is going to be used on decent sized systems) that separate
compilation (and separate proof) be supported, and for that *only* the contracts
matter (because looking inside of bodies outside of the current unit is not
allowed). Mixing in non-contracts is just going to confuse as to what can and
cannot be depended on.

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

From: Robert Dewar
Sent: Thursday October 27, 2011  10:34 PM

> Indeed, I would argue that using a contract feature for reasons
> unrelated to contracts is likely to be confusing and maybe even
> harmful. I understand the need for proof features, but these should
> not get mixed with contracts. It's important (if proof is going to be
> used on decent sized systems) that separate compilation (and separate
> proof) be supported, and for that *only* the contracts matter (because
> looking inside of bodies outside of the current unit is not allowed).
> Mixing in non-contracts is just going to confuse as to what can and cannot be
> depended on.

For a different take on this issue, see the Hi-Lite project
> http://www.open-do.org/projects/hi-lite/

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

From: Robert Dewar
Sent: Thursday October 27, 2011  9:33 PM

> Thus, pre and post aren't allowed on bodies. If checks are needed in
> the body that aren't known to the caller, we have pragma Assert for
> that purpose. (In addition, it's often possible to add abstractions to
> use in the pre and post conditions. Those needn't add much cost if
> they are modeled as expression functions or otherwise inlined.)

The reason that precondition and postcondition (the GNAT pragmas) are nice in
bodies, is, particularly in the postconditoinc ase, the ability to talk about
the return value, and the old values of parameters.

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  9:45 PM

Huh? The 'Old and 'Result attributes are allowed in postconditions given in
specifications; in particular, Param'Old is allowed, as is Func'Result. No need
to put the postcondition in the body for that.

I could imagine that a case similar to the one Steve gave would make some sense,
especially if using 'Old on a package body variable. But that seems more like an
assertion to me, and as I argued a minute ago, I think it is valuable to keep
the real contracts separated from assertions.

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

From: Robert Dewar
Sent: Thursday October 27, 2011  10:37 PM

> Huh? The 'Old and 'Result attributes are allowed in postconditions
> given in specifications; in particular, Param'Old is allowed, as is
> Func'Result. No need to put the postcondition in the body for that.

No need for a Huh? when the issue is simply that you have missed the point :-)

The point is that yes, asserts can largely take the place of preconditions and
postconditions in the body (we are NOT talking about pre/post conditions given
with the spec, but those appearing in the body, referencing things for example
that only the body can see). It is in this situation that being able to use
'Result and 'Old in such postconditions in the body is more convenient than
having to do this manually

> I could imagine that a case similar to the one Steve gave would make
> some sense, especially if using 'Old on a package body variable. But
> that seems more like an assertion to me, and as I argued a minute ago,
> I think it is valuable to keep the real contracts separated from assertions.

Doing postconditions with assertions in the body is messy, because you have to
find and block all return points.

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

From: Randy Brukardt
Sent: Thursday October 27, 2011  11:07 PM

> > Huh? The 'Old and 'Result attributes are allowed in postconditions
> > given in specifications; in particular, Param'Old is allowed, as is
> > Func'Result. No need to put the postcondition in the body for that.
>
> No need for a Huh? when the issue is simply that you have missed the
> point :-)
>
> The point is that yes, asserts can largely take the place of
> preconditions and postconditions in the body (we are NOT talking about
> pre/post conditions given with the spec, but those appearing in the
> body, referencing things for example that only the body can see). It
> is in this situation that being able to use 'Result and 'Old in such
> postconditions in the body is more convenient than having to do this
> manually

I don't think I missed the point so much as you didn't make it. :-) Steve had
mentioned hidden objects, but your reply was all about "old values of
parameters". Hard to make a connection from that.

> > I could imagine that a case similar to the one Steve gave would make
> > some sense, especially if using 'Old on a package body variable. But
> > that seems more like an assertion to me, and as I argued a minute
> > ago, I think it is valuable to keep the real contracts separated
> > from assertions.
>
> Doing postconditions with assertions in the body is messy, because you
> have to find and block all return points.

That's what "finally" (or "at end") is for. Pity that Ada doesn't have it -- I'd
rather add that than a somewhat dubious body postcondition.

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

From: Robert Dewar
Sent: Friday October 28, 2011  6:23 AM

> I don't think I missed the point so much as you didn't make it. :-)
> Steve had mentioned hidden objects, but your reply was all about "old
> values of parameters". Hard to make a connection from that.

Fair enough

> That's what "finally" (or "at end") is for. Pity that Ada doesn't have
> it -- I'd rather add that than a somewhat dubious body postcondition.

Well I see nothing dubiuos about such a post-condition, but I agree this would
be a nice feature in Ada as an alternative approach, and sometimes things would
feel better as a postcondition to me, and sometimes as an at end, e.g. making
sure a file is closed.

Note that it would be amazingly easy to implement "at end" in GNAT, since
internally we have exactly that construct. It is a little tricky to decide what
to do in the case where you have both exception handlers and "at end",
internally in GNAT we allow one or the other but not both in a single block (and
generate appropriate nested blocks where needed).

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

From: John Barnes
Sent: Friday October 28, 2011  4:21 AM

Spark allows pre and postconditions in bodies to support refinement. They
(should be) still the same condition just a different view of it.

But they are allowed in a body if there is no spec.

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

From: John Barnes
Sent: Friday October 28, 2011  4:32 AM

>> Generic instantiations need to fit into this.
>>
>>     procedure Conv is new Ada.Unchecked_Deallocation(Obj, Ptr)
>>       with Inline;
>>
>> is more readable to me than
>>
>>     procedure Free with Inline is new Ada.Unchecked_Deallocation(Obj, Ptr);


Agreed

> Sure, but that's not how you'd format it:
>
>      procedure Free
>         with Inline
>         is new Ada.Unchecked_Deallocation(Obj, Ptr);
>

That's really horrid. Although I split instantiations over several lines I
always break after is and not before it.

> Aside: No matter what rule we adopt, we need a simple explanation of
> it, and John should have that explanation in the Rationale. It
> shouldn't be necessary to think of it as a hodge-podge...


Clearly "its part of the spec" is important. Otherwise, readability seems to
be a prime objective.

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

From: Robert Dewar
Sent: Friday October 28, 2011  6:45 AM

>>> Generic instantiations need to fit into this.
>>>
>>>      procedure Conv is new Ada.Unchecked_Deallocation(Obj, Ptr)
>>>        with Inline;
>>>
>>> is more readable to me than
>>>
>>>      procedure Free with Inline is new
>>> Ada.Unchecked_Deallocation(Obj,
>> Ptr);
>>
>
> Agreed

Right, indeed Inline belongs at the end, it is kind of an implementation after
thought, not a critical part of the spec needed up front. Indeed I often prefer
to put pragma Inline's in the private part for visible subprograms, it's really
none of the caller's business.

Perhaps we should always allow aspects in both syntactic positions, at least
that would be a simple rule :-)

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

From: John Barnes
Sent: Friday October 28, 2011  5:28 AM

>> John should have that explanation in the Rationale. It shouldn't be
>> necessary to think of it as a hodge-podge...

> Clearly "its part of the spec" is important. Otherwise, readability
> seems to be a prime objective.

At the moment that part of the draft rationale says

The appropriate layout should be obvious. In the case of a structure that has a
specification and body, the aspect specification goes with the specification
before is. The only case where a body can have an aspect specification is a
subprogram without a separate body in which case the aspect goes before the is
of the body. But when something is all in one piece such as a null procedure,
object declaration or generic instantiation any aspect specification goes at the
end of the declaration; it is then more visible and less likely to interfere
with the layout of the rest of the structure.

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

From: Jean-Pierre Rosen
Sent: Friday October 28, 2011  5:38 AM

> The appropriate layout should be obvious. In the case of a structure
> that has a specification and body, the aspect specification goes with
> the specification before is. The only case where a body can have an
> aspect specification is a subprogram without a separate body in which
                                                          ^^^^ spec

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

From: John Barnes
Sent: Friday October 28, 2011  11:35 AM

Merci beaucoup JP.  Interesting how most people read what they expect to see.

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

From: Robert Dewar
Sent: Friday October 28, 2011  6:52 AM

> At the moment that part of the draft rationale says
>
> The appropriate layout should be obvious. In the case of a structure
> that has a specification and body, the aspect specification goes with
> the specification before is. The only case where a body can have an
> aspect specification is a subprogram without a separate body in which
> case the aspect goes before the is of the body. But when something is
> all in one piece such as a null procedure, object declaration or
> generic instantiation any aspect specification goes at the end of the
> declaration; it is then more visible and less likely to interfere with
> the layout of the rest of the structure.

Seems a clear enough rationale and rule to me!

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

From: Robert Dewar
Sent: Friday October 28, 2011  6:43 AM

As an example of preconditions/postconditions in the body consider a memo
function.

The function is supposed to do two things, properly return the right result
(spec post condition), and properly update the memo global data (body post
condition).

In addition, it checks that its parameters are reasonable (spec precondition),
and that the memo data is in ok shape (body precondition).

Yes, you can do everything with assertions (even spec pre/post conditions can be
modeled this way), but it is cleaner and clearer to be able to use pre/post
conditions in both the spec and body.

As I say, GNAT already has this capability in full generality, so it doesn't
particularly concern me that it is lacking in the standard.

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

From: Jean-Pierre Rosen
Sent: Friday October 28, 2011  7:10 AM

> As an example of preconditions/postconditions in the body consider a
> memo function.
>
There are really two ways of seeing things here:
1) Pre/Post are a contract between the client and the provider of the service.
   In this case, the memo implementation is invisible and pre/post in the body
   are irrelevant

2) Pre/post are intended to prove correct behaviour of the implementation. Then,
   body pre/post make sense.

My understanding is that the requirement for Ada 2012 was 1).

Should we add 2)? TBH, I don't know. Waiting for other voices.

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

From: Robert Dewar
Sent: Friday October 28, 2011  7:26 AM

> Should we add 2)? TBH, I don't know. Waiting for other voices.

I would think it is a bit late to add 2) at this stage. The question before even
considering this would be:

if we allow Pre/Post on subprogram bodies, which have separate specs (I don't
really care about the silly case of no separate spec), then are there any
adverse subtle consequences? If so, I would say drop it, if there are really no
problems at all, then it might be worth considering even at this late date (it
would be easy to implement in GNAT, we would just remove the arbitrary rule that
forbids Pre/Post in bodies :-))

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

From: Bob Duff
Sent: Friday October 28, 2011  7:30 AM

> Should we add 2)? TBH, I don't know. Waiting for other voices.

IMHO, we shouldn't be adding new features at this point, especially if some
folks don't like them and/or don't see the need.

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

From: Randy Brukardt
Sent: Friday October 28, 2011  12:44 PM

> There are really two ways of seeing things here:
> 1) Pre/Post are a contract between the client and the provider of the
> service. In this case, the memo implementation is invisible and
> pre/post in the body are irrelevant
>
> 2) Pre/post are intended to prove correct behaviour of the
> implementation. Then, body pre/post make sense.
>
> My understanding is that the requirement for Ada 2012 was 1).
>
> Should we add 2)? TBH, I don't know. Waiting for other voices.

I think there is value in using separate (perhaps related) constructs for
(1) and (2), so there is no confusion to the clients as to what they can depend
on in calls. So I would not want to see any extensions to the existing features.

(And it's too late to find Robert's "subtle consequences" with any level of
certainty. It might be FUD, but we're close enough to the finish line that FUD
is the right approach.)

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

From: Erhard Ploedereder
Sent: Friday October 28, 2011  9:16 AM

To sum up my intent: Short of any good arguments still being voiced in favor of
aspects on bodies, I would like to shorten the present rule

35/3
 An aspect shall not be specified in an aspect_specification given on a
 subprogram_body that is a completion of another declaration.

to

 An aspect shall not be specified in an aspect_specification given on a
 subprogram_body.

Rationale:
Anybody can write a spec if he/she needs aspects. The rule avoids the slightly
bothersome syntax permutation on "is..." as discussed earlier. The rule is
simple to remember and teach.

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

From: Robert Dewar
Sent: Friday October 28, 2011  9:29 AM

I still prefer that we can have aspects on any declaration, since who knows what
the requirements are for implementation defined aspects.

Do we really want to prohibit an implementation from adding Body_Pre and
Body_Post attributes for pre/postconditions in bodies?

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

From: Tucker Taft
Sent: Friday October 28, 2011  9:36 AM

I agree we should err on the side of leaving things out at this stage, not
adding in new things.

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

From: Robert Dewar
Sent: Friday October 28, 2011  9:42 AM

I agree, but to me the "new things" should include any attempts to limit what is
now allowed :-)

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

From: Erhard Ploedereder
Sent: Friday October 28, 2011  12:13 PM

> Do we really want to prohibit an implementation from adding Body_Pre
> and Body_Post attributes for pre/postconditions in bodies?

Presently we do prohibit them, if there is a subprogram spec.

.. and we allow them if there is no separate spec.

which is more or less equal to saying:
implementations with specs that are globally visible can have no aspects on
their bodies. Only local subprograms can have them.

A strange rule indeed.

On the question itself: I find invisible Pre- and Postconditions a contradiction
in terms. The very reason for having them is to visibly describe behavior. All
else can be done with Assertions and suchlike.

Pre- and Postconditions are concepts of contract to me, not arbitrary assertion
concepts for expressing what is true at the beginning and the end. (I readily
agree that there are such additional assertions that are a consequence of
implementation, of no concern to the caller, but of concern to the implementer.
I just don't believe into heaping them into the pre-/postcondition basket.)

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

From: Erhard Ploedereder
Sent: Friday October 28, 2011  12:21 PM

Ok, before someone complains, I forgot separately compiled bodies without spec. But the advice: "you want aspects, you compile it separately" is too bad to even mention ;-)

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

From: Randy Brukardt
Sent: Friday October 28, 2011  12:40 PM

> Do we really want to prohibit an implementation from adding Body_Pre
> and Body_Post attributes for pre/postconditions in bodies?

The original reason we added the capability on subprogram bodies was so that
main subprograms don't need a separate specification to define a priority, CPU,
deadline, and the like. A separate specification for main subprograms is
somewhat weird, and probably would cause a lot of programmers to stick with the
pragmas rather than the aspects.

But I also agree with Robert's point. If some sort of body postcondition is
useful for proofs, then it would make sense to add such an aspect. (It would
need to override the current blanket rule for aspects, but of course any aspect
can do that, and any impl-def aspect can have whatever rules it likes.) We
shouldn't be disallowing that -- we allow almost anything goes.

However, that brings up a different question: we don't allow aspects on stubs or
other bodies (packages, tasks). Robert's principle here would suggest that we
ought to.

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

From: Robert Dewar
Sent: Friday October 28, 2011  3:34 PM

> On the question itself: I find invisible Pre- and Postconditions a
> contradiction in terms. The very reason for having them is to visibly
> describe behavior. All else can be done with Assertions and suchlike.

But inconveniently! As I have pointed out several times it is very awkward to
use assertions for implementation postconditions, since you don't have 'Result
and 'Old, and you have to find all return points, and do a significant bit of
rewriting (to deal with not having 'Result).

And if you were doing it in your own implementation, you could follow the
thought below and add the new aspects and call them something like
Assert_On_Entry and Assert_On_Exit. The point is that it is valuable to be
*able* to invent such impl defined aspects, rather than forcing implementations
to use pragmas instead.

(I find myself somewhat inclined to stick with the pragmas in my own GNAT code,
since that way I can use the same syntax for specs and bodies, which to me seems
prefrable).

> Pre- and Postconditions are concepts of contract to me, not arbitrary
> assertion concepts for expressing what is true at the beginning and
> the end. (I readily agree that there are such additional assertions
> that are a consequence of implementation, of no concern to the caller,
> but of concern to the implementer.
> I just don't believe into heaping them into the pre-/postcondition
> basket.)

Note that in GNAT, precondition and postcondition pragmas can appear both in the
spec and body. We did not invent this out of the blue, a major customer (and
major user of Ada) wanted exactly this capability.

BTW, that's also a response to Steve's bogus claim [filed as a separate thread
below - Editor] that pre/postconditions are ONLY interesting in the context of
formal proofs. This same customer was VERY interested in having
preconditions/postconditions that work the way they do in Ada (which after all
is not that different from the way they are in Eiffel).

For an interesting project which attempts to figure out how to combine the two
different views of preconditions and postconditions (run time tersts, and aids
for formal proving), and in general how to combine testing and proofs, see the
hi-lite project:

> http://www.open-do.org/projects/hi-lite/

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

From: Jean-Pierre Rosen
Sent: Saturday October 29, 2011  3:10 PM

Here is a suggestion:

1) Keep Pre/Post as intended (the external view contract)
2) State that /language defined/ aspects are not allowed on a body if there is
   an explicit spec (and presumably, never allowed on separate proper bodies)

This leaves an implementation with the possibility of defining its own aspects
the way it wants (hint: Implementation_Pre and Implementation_Post for example)

Note that for Ada 2019, it would be easy if necessary to change 2) into:
Unless otherwise specified, /language defined/ aspects are not allowed etc.

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

From: Robert Dewar
Sent: Saturday October 29, 2011  11:23 PM

By the way, in GNAT, our decision on pre/postcondition pragmas isthat if you
want spec (caller contract) pre/post conditions, you MUST have a separate spec,I
think this is perfectly reasonable, and I see no reason to allow ANY spec
aspects on bodies lacking a spec.

It just seems plain horrible to me to have different rules for aspects on bodies
depending onwhether there is a separate spec.

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

From: John Barnes
Sent: Monday October 31, 2011  3:13 AM

>Note that for Ada 2019, it would be easy .....

Count me out. I will be over 81 and in that death and decay phase of life (if
not already)!

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

From: Stephen Michell
Sent: Friday October 28, 2011  10:07 AM

>> I agree that the contract is one of the reasons. The other reason is
>> ...
>
> Sorry, there is no other reason. Pre and post conditions in Ada 2012
> are purely contract features. Any resemblance to any other feature,
> living or dead :-), is purely coincidental.
>
> Indeed, I would argue that using a contract feature for reasons
> unrelated to contracts is likely to be confusing and maybe even
> harmful. I understand the need for proof features, but these should
> not get mixed with contracts. It's important (if proof is going to be
> used on decent sized systems) that separate compilation (and separate
> proof) be supported, and for that *only* the contracts matter (because
> looking inside of bodies outside of the current unit is not allowed).
> Mixing in non-contracts is just going to confuse as to what can and cannot be
> depended on.

But a contract feature is useless if it cannot be formally shown to be true v

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

From: Randy Brukardt
Sent: Friday October 28, 2011  1:05 PM

That is an extreme viewpoint; it seems to say that dynamic constraints (for
example) are useless. Dynamic checks have plenty of value.

And we decided from the very beginning that Ada's contract features are intended
for dynamic checks. Any ability to use them for formal proofs is a happy
accident, not something that was intended.

I'm willing match your extreme viewpoint with one of my own: proofs that depend
on anything *other* than contracts are of little value outside of toy programs.
And I don't think complete proofs are worth the effort(*). I want to be able to
prove important properties (like absence of exceptions that violate an exception
contract) at compile-time, and that means looking in bodies is not  allowed.

(*) My guess is that if most programmers are faced with the task of defining a
complete, provable postcondition for a subprogram, they would end up making a
copy of the internal algorithm. That does not add value (especially if the
postcondition language is also Ada), it just takes time. In the sorts of
subprograms that I often write, there are a few high-level effects that can and
should be described in a postcondition, but the details are not worth the
effort.

Consider the subprogram that adds the declaration of a variable to the symbol
table. Something like
    procedure Add_Var (Decl : in Tree; New_Variable : out Symbol_Ptr);
It would make sense that the postcondition include Is_Newly_Added(New_Variable)
and Name(New_Variable) = Decl.Id. But trying to describe all of the properties
of an object (there are about 30 in Janus/Ada) would just be a waste of time --
the code would end up being a copy of the body of Add_Var. It would add nothing
but complexity.

So I doubt that there is much value to *complete* formal proofs in a large
system. OTOH, there is a lot that can be done with whatever information the
programmer puts into the contract, even if the proof is not complete. It's that
value (which can directly detect bugs before they happen) that I care about.

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

From: Stephen Michell
Sent: Friday October 28, 2011  1:55 PM

We should not be arguing the relative merits of static vs dynamic verification.
The point is that the body always knows more about the state of the program than
the spec does, and the formal relationship between the preconditions, state,
processing and postconditions can be simplified once you can see the "hidden"
parts. We need to be able to express these relationships in ways that make
verification easier. Artificially prohibiting pre and postconditions on bodies
makes our work much harder.

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

From: Robert Dewar
Sent: Saturday October 29, 2011  6:55 AM

> We should not be arguing the relative merits of static vs dynamic
> verification.

I agree, but it was you (Stephen) who raised this issue :-)

> The point is that the body always knows more about the state of the
> program than the spec does, and the formal relationship between the
> preconditions, state, processing and postconditions can be simplified
> once you can see the "hidden" parts. We need to be able to express
> these relationships in ways that make verification easier.
> Artificially prohibiting pre and postconditions on bodies makes our
> work much harder.

I don't know how artificial that is. But right now, the situation is that in Ada
2012 we regard preconditions and postconditions purely in the Eiffel style, as
contracts between the caller and the callee, and obviously both parties must
know about a contract, hence Pre and Post conditions are confined to specs.

I have agreed that preconditions and postconditions are useful in bodies as
well, but three points:

a) it is far too late to add this capability to Ada 2012. In particular, if we
   just add a permission to have Pre/Post on bodies, I would guess that there
   will be semantic ramifications we do begin to have time to deal with (i.e.
   this is not just an artificial restriction).

b) there is far from a consensus that such an addition is appropriate. At least
   some feel that it is appropriate to restrict preconditions and postconditions
   to the "caller contract" model, and object to adding this capability to
   bodies, regardless of difficulties in definition.

c) in practice, the initially widely available implementation of Ada 2012 will
   allow precondition and postcondition pragmas to appear in bodies, meaning
   that people can experiment with their use in this context.

So I say, let's keep things as they are, and we can revisit this later on if it
seems appropriate to do so.

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

From: Steve Michell
Sent: Saturday October 29, 2011  1:27 PM

I think that is is the best that we can do for now.

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

From: Dan Eilers
Sent: Saturday October 29, 2011  11:56 AM

The argument in c) (which I agree with) that no other vendor finds sufficient
merit in the proposed Ada 2012 amendments to actually implement most of then
them anytime soon seriously undermines the argument in a) that there is some
reason to rush to standardize these amendments.

We are due for an Ada 2005 corrigendum soon, to correct the numerous errors in
Ada 2005.  It was 6 years from publication of Ada 95 to publication of the
corrigendum in 2001.  6 years from the publication of Ada 2005 (in 2007) puts
the Ada 2005 corrigendum's expected date in 2013.  There is however no urgent
need for an Amendment anytime soon, especially when all but one vendor is voting
with their feet against it, based on their assessments of what the market is
interested in.

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

From: Robert Dewar
Sent: Saturday October 29, 2011  1:47 PM

I strongly disagree with this. There are numerous reasons to press ahead with
the Ada 2012 standard in my view.

The perception of continued development and change is important to the continued
viability of Ada, and is a big help to our friends who are Ada advocates.

Ada 2012 is widely known as such at this stage, and it would be perceieved as
unfortunate if it got delayed.

I don't see any vital issues that would generate a consensus for a delay, quite
the opposite in fact, it seems like most people are of a mind to stick with the
schedule.

Finally, and most importantly, "assessments of what the market is interested in"
are quite strongly related to what in fact the market is interested in. This
interest is driven by competition, and the availability of an implementation for
Ada 2012 which is available at the same time of the standard will help drive
customer demand, and is precisely the factor that is needed to get other vendors
moving.

For example, I don't think Rational would have announced Ada 2005 if it had not
been for their customers expressing interest in Ada 2005, and the fact that
those customers had an alternative path to Ada 2005 acted as a useful push.

The fact that rational now has Ada 2005 of course heats up the competition,
which is certainly fine for rational, fine for its customers, and ultimately
fine for everyone, including AdaCore, even if it takes away a marketing
advantage.

The "numerous errors" in Ada 2005 may concern language lawyers but they don't
concern users (or for that matter implementors) to any significant degree. It is
much more important to get out the significant new features of Ada 2012 than to
tinker around fixing minor problems of no consequence in Ada 2005.

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

From: Erhard Ploedereder
Sent: Saturday October 29, 2011  5:14 AM

After an evening of thinking about the problem (occasionally): I agree with
Randy whole-heartedly. I have no issue with "body pre-/post-conditions" to
reflect implementation properties, as long as they are syntactically
distinguished from those that are addressed to the client (and restricted to
appear only in the respective constructs - for  bi-sexual constructs, both are
allowed, of course.)

I can envisage two solutions: 1. Add two more aspects with new names that
express the idea (obviously the most general solution).

2. The only time this matters is on bodies acting as specs as well.
Otherwise the location distinguishes the two kinds of conditions.
Hence forbidding aspects on those is a crude but effective mechanism to
distinguish the two kinds of pre- and postconditions. And if folks have to spec
their Main occasionally, so what ?

P.S. Addressed to Steven: Sure, one would like to verify the contractual
pre- and postconditions. But this does not depend on the existence of
implementation pre- and postconditions, since the very same information can be
captured in general Assertions. Whether one calls an assertion a pre- or
postcondition does little to alter its semantics. A verification model that
presumes that ALL information (including identities) needs to be carried into
and across calls with pre- and post-conditions will not scale at all.
Admittedly, if you have the all-encompassing pre-/postconditions in mind that
you need in a Hoare or Floyd calculus to carry the World-knowledge across calls,
then you are right in cramming everything into these predicates. But does that
scale at all? My view from 30 years ago and still unchanged is that this model
has hindered progress in verification substantially (and unnecessarily).
Dijkstra was right about his weakest/strongest pre-/postconditions, which
eliminated this restriction a long time ago.

You might say: so why not put needed knowledge into pre-/post- at the
implementation level, rather than into general assertions? I would not object
(anymore) if there were a clear distinction between preconditions whose truth is
the responsibility of the caller (i.e., contractual preconditions) and
preconditions whose truth is the responsibility of the implementer of a set of
connected routines (i.e., implementation invariants).

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

From: Erhard Ploedereder
Sent: Saturday October 29, 2011  7:10 PM

> And if you were doing it in your own implementation, you could follow
> the thought below and add the new aspects and call them something like
> Assert_On_Entry and Assert_On_Exit. The point is that it is valuable
> to be *able* to invent such impl defined aspects, rather than forcing
> implementations to use pragmas instead.

As I said in a later message, I changed my mind about implementation
pre/postconditions, but I do want them syntactically distinguished from spec
pre/post conditions that need to be established/observed by the caller. Your
argument about multiple returns is very convincing. I certainly would be happy
with a language-defined Assert_On_Entry/Assert_On_Exit pair for them.

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

From: Robert Dewar
Sent: Tuesday November 1, 2011  9:37 AM

Yes, that's probably nicer than reusing pragma Postcondition and pragma
Precondition in the body, but now we are stuck with those pragmas in GNAT,
perhaps we should allow Assert_On_Entry and Assert_On_Exit as alternative names
(or even aspects).

Anyway, I think it is too late to try to add this to the Ada2012 definition at
this stage???

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

From: Erhard Ploedereder
Sent: Wednesday November 2, 2011  2:01 PM

I don't know. The situation with the placement of the aspects in "bodies as
specs" vis-a-vois the "is" has not been resolved.

We drifted into this (worthwhile but still peripheral) discussion of spec vs
body pre/postconditions and I think additional unintentional nastiness has been
discovered (e.g., if you don't use a subprog spec, you can refer to body
internals in pre-/postconditions. Exactly the opposite of what good advice
should look like.)

Maybe both should be a topic at the upcoming meeting. Ed ?

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

From: Jean-Pierre Rosen
Sent: Wednesday November 2, 2011  2:15 PM

My understanding is that as soon as the document has been submitted to NB, all
comments should come from the NB (but are still doable).

Therefore, we should discuss remaining issues at the ARG meeting, but any change
we decide has to come from some NB (there are enough of us involved with their
NB to spread the "comments" over various nations)

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

From: Robert Dewar
Sent: Wednesday November 2, 2011  2:20 PM

> We drifted into this (worthwhile but still peripheral) discussion of
> spec vs body pre/postconditions and I think additional unintentional
> nastiness has been discovered (e.g., if you don't use a subprog spec,
> you can refer to body internals in pre-/postconditions.
> Exactly the opposite of what good advice should look like.)

I don't think that's the case at all, I don't think these pre and post have any
more visibility than the caller does.

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

From: Edmond Schonberg
Sent: Wednesday November 2, 2011  2:48 PM

We should certainly come to a consensus on this in Denver. It will be on the
agenda.

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

From: Randy Brukardt
Sent: Wednesday November 2, 2011  5:09 PM

Way ahead of you. Created and posted an AI last night.

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

From: Erhard Ploedereder
Sent: Wednesday November 2, 2011  7:10 PM

> I don't think that's the case at all, I don't think these pre and post
> have any more visibility than the caller does.

As I wrote my mail, I started thinking about that, too.

Presumably, at a minimum, implementation aspects/pragmas would have visibility
of private type completions that the aspects on the spec cannot see. Anything
else? Stephen?

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

From: Robert Dewar
Sent: Wednesday November 2, 2011  7:05 PM

Well we are talking not about implementation aspects Post and Pre etc predefined
in the language, but rather the use of these on the body when there is no spec.
I agree it's unclear what they can see.

I really MUCH prefer we just ban Pre/Post etc aspects on a subprogram body
period. If people want these aspects they MUST write a spec, that seems a
perfectly reasonable rule.

Bodies with no specs are warts, and we should not waste time on additional
makeup to cover them up!

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

From: Erhard Ploedereder
Sent: Wednesday November 2, 2011  7:58 PM

That is exactly were I was standing a few days ago - and it is of course not the
state of Draft 14.

Then came some Robert D., who made a convincing argument that there should be
Pre/Post on bodies as well ("multiple returns", interaction with exceptions,
etc. etc.). An evil twin? :-) Admittedly you argued for impl-defined ones,
because you already have them in the form of pragmas. But if they are needed,
they are not precarious to add to the language itself, as long as the two kinds
are kept well separated.

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

From: Robert Dewar
Sent: Wednesday November 2, 2011  8:10 PM

I was NOT arguing for adding these to the language, merely for keeping the
possibility of adding impl-defined ones. We have two separate issues here and
you are I think confusing them.

For contract Pre/Post aspects, normally on the spec, because they must be
visible to the caller, are we allowed to park them on the body when there is no
spec? The definition currently says yes, I think this is a confusing mistake,
which should be rectified by the simple method of saying NO to this quesation.

Totally separate issuee, should there be some kind of Pre/Post capability on
bodies?

Maybe yes, but robert thinks

a) it is too late to stick that in the standard

b) we should allow impl defined aspects on bodies so that implementors can add
   this capability if they like.

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

From: Randy Brukardt
Sent: Monday November 7, 2011  6:01 PM

...
> For contract Pre/Post aspects, normally on the spec, because they must
> be visible to the caller, are we allowed to park them on the body when
> there is no spec? The definition currently says yes, I think this is a
> confusing mistake, which should be rectified by the simple method of
> saying NO to this quesation.

We allow aspects on subprogram bodies so that aspects like Priority can be
specified on bodies without requiring a separate specification. (That would be
weird for a main subprogram, which is the only kind of subprogram that can have
Priority.)

We use the same rules for all aspects, but of course there is no requirement to
do that.

But I have to admit, I don't see any problem here. If you put Pre on a body
(that has no spec), it is true that the precondition can see private
declarations. But that's not a problem, since any caller *also* has to be able
to see those declarations (since if they can see the subprogram body, they can
also see the private declarations). So it is fine to allow such in the
preconditions.

If someone later adds a separate specification, the precondition would have to
move and be changed, but that seems like a different situation.

So I don't think we need a change here.

> Totally separate issuee, should there be some kind of Pre/Post
> capability on bodies?
>
> Maybe yes, but robert thinks
>
> a) it is too late to stick that in the standard

Agreed.

> b) we should allow impl defined aspects on bodies so that implementors
> can add this capability if they like.

That's already true, as any aspect (including language-defined ones) is allowed
to invent its own rules, and surely that's the case for implementation-defined
aspects.

The only open questions [related to that] that I know of is (1) should we allow
aspect_specifications on stubs? Presumably with similar rules to bodies (2)
should we allow aspect_specifications on package/task/protected bodies, only for
implementation-defined aspects. I lean toward "Yes" on both of these questions,
especially as we already did the latter for renames and generic formal
parameters (no language-defined aspects, but the clause is allowed). Don't see
much reason for these other things to be different.

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

From: Robert Dewar
Sent: Monday November 7, 2011  6:06 PM

> But I have to admit, I don't see any problem here. If you put Pre on a
> body (that has no spec), it is true that the precondition can see
> private declarations. But that's not a problem, since any caller
> *also* has to be able to see those declarations (since if they can see
> the subprogram body, they can also see the private declarations). So
> it is fine to allow such in the preconditions.

OK

> If someone later adds a separate specification, the precondition would
> have to move and be changed, but that seems like a different situation.
>
> So I don't think we need a change here.

OK, not a big deal for me

>> Totally separate issuee, should there be some kind of Pre/Post
>> capability on bodies?
>>
>> Maybe yes, but robert thinks
>>
>> a) it is too late to stick that in the standard
>
> Agreed.
>
>> b) we should allow impl defined aspects on bodies so that
>> implementors can add this capability if they like.
>
> That's already true, as any aspect (including language-defined ones)
> is allowed to invent its own rules, and surely that's the case for
> implementation-defined aspects.

OK, was just reacting to one suggestion of taking this away

> The only open questions [related to that] that I know of is (1) should
> we allow aspect_specifications on stubs? Presumably with similar rules
> to bodies (2) should we allow aspect_specifications on
> package/task/protected bodies, only for implementation-defined
> aspects. I lean toward "Yes" on both of these questions, especially as
> we already did the latter for renames and generic formal parameters
> (no language-defined aspects, but the clause is allowed). Don't see much
> reason for these other things to be different.

I agree with randy on this

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