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