Version 1.2 of ai05s/ai05-0267-1.txt
!standard 13.3.1(0) 11-11-01 AI05-0267-1/01
!class Amendment 11-11-01
!status work item 11-11-01
!status received 11-10-26
!priority Low
!difficulty Medium
!subject Improvements for aspect specifications
!summary
** TBD.
!proposal
(1) The syntax for aspect_specifications seems inconsistent for subprograms.
In particular, the aspect_specifications occur before "is" for bodies,
and after "is" for abstract subprograms, null procedures, and expressions
functions.
Change this? (No.)
(2) We don't allow aspect_specifications on subprogram stubs currently.
That requires adding an extra declaration in order to put preconditions, etc. on
such items. We probably should adopt the same rules/syntax for stubs as we do
subprogram bodies. Specifically, we should allow aspect_specifications on a
stub IFF there is no subprogram specification (and in that case, they are
not allowed on the body).
(3) Some (yet-to-be-defined) aspects may make sense on bodies (even if there
is a specification). For subprograms, the syntax is already there, so there is
no problem. But for other program units, we are only allowing aspects on the
specification. It was suggested to allow the syntax on bodies, and also
add a bit of wording to essentially say that no language-defined aspects are
allowed there. We already have a precident for that, as there aren't any
aspects allowed on generic formal types (but we do allow the syntax for
future use).
(4) There was some discussion of body preconditions and postconditions.
The former can easily be modeled with an assert pragma, but the later cannot
because of the 'Old and 'Result attributes and the possibility of multiple
exits. We don't want to call these things "postconditions" as that is a
contract thing and we want to keep contracts separate from other proof
aids. It was suggested to allow aspects Assert_on_Entry and Assert_on_Exit
on subprogram bodies, and allow the 'Old and 'Result attributes in the latter.
!wording
** TBD.
!discussion
(1) For this, a principle was given that aspect_specifications go at the
end of declarations, other than program units and bodies (where they go before
"is".
This principle should be added to the AARM as a "Language Design Principle",
so that future Ada designers can figure out what the heck we were thinking.
John suggested:
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 specification 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.
[I think we can do better than this, and surely we should drop the first
sentence from an AARM note. But it's a good start - Editor.]
(2) This seems important for consistency.
(3) This seems like a good idea for future flexibility. [But it will require
enough wording changes that it might be too late - Editor.]
(4) This is a good idea. But it seems to be too late for Ada 2012; there is
no way to consider the semantic ramifications or edit the wording. [Best
to make an Ada 2012 AI?? - Editor]
!ACATS test
** TBD.
!ASIS
No ASIS effect. (??)
!appendix
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: 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.
****************************************************************
[Editor's note: There are at least another 40 messages in this thread.
Hopefully, I'll get those filed soon.]
Questions? Ask the ACAA Technical Agent