CVS difference for ai05s/ai05-0267-1.txt

--- ai05s/ai05-0267-1.txt	2011/11/02 05:27:28	1.2
+++ ai05s/ai05-0267-1.txt	2011/11/09 03:21:25	1.3
@@ -1669,6 +1669,13 @@
 
 ****************************************************************
 
+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
 
@@ -1756,7 +1763,715 @@
 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.
 
-[Editor's note: There are at least another 40 messages in this thread.
-Hopefully, I'll get those filed soon.]
+****************************************************************
+
+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
+
+****************************************************************