!standard 13.1.1(0) 11-12-21 AI05-0267-1/02 !standard 7.2(2) !standard 9.1(6) !standard 9.4(7) !standard 10.1.3(3/2) !standard 10.1.3(4) !standard 10.1.3(5) !standard 10.1.3(6) !class Amendment 11-11-01 !status Amendment 2012 11-12-21 !status ARG Approved 8-0-1 11-11-12 !status work item 11-11-01 !status received 11-10-26 !priority Low !difficulty Medium !subject Improvements for aspect specifications !summary Allow aspect_specifications on stubs and all bodies. Language-defined aspects are allowed only on stubs that do not have separate specifications; they are never allowed on bodies. !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). Add aspect_specifications to stubs? (Yes.) (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 precedent for that, as there aren't any aspects allowed on generic formal types (but we do allow the syntax for future use). Add aspect_specification to bodies? (Yes.) !wording Replace 7.2(2): package_body ::= package body defining_program_unit_name [aspect_specification] is declarative_part [begin handled_sequence_of_statements] end [[parent_unit_name.]identifier]; Replace 9.1(6): task_body ::= task body defining_identifier [aspect_specification] is declarative_part begin handled_sequence_of_statements end [task_identifier]; Replace 9.4(7): protected_body ::= protected body defining_identifier [aspect_specification] is { protected_operation_item } end [protected_identifier]; Replace 10.1.3(3/2): subprogram_body_stub ::= [overriding_indicator] subprogram_specification is separate [aspect_specification]; Replace 10.1.3(4): package_body_stub ::= package body defining_identifier is separate [aspect_specification]; Replace 10.1.3(5): task_body_stub ::= task body defining_identifier is separate [aspect_specification]; Replace 10.1.3(6): protected_body_stub ::= protected body defining_identifier is separate [aspect_specification]; Add after 13.1.1(16/3): There are no language-defined aspects that may be specified on a renaming_declaration, a generic_formal_parameter_declaration, a subunit, a package_body, a task_body, a protected_body, or a body_stub other than a subprogram_body_stub. A language-defined aspect shall not be specified in an aspect_specification given on a subprogram_body or subprogram_body_stub that is a completion. Delete 13.1.1(34-35/3) [moved above]. !discussion (1) For this, a principle was given that aspect_specifications go at the end of declarations, other than program units (that are not subprogram specifications) 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. Syntactically, aspect_specifications generally are located at the end of declarations. When a declaration is all in one piece such as a null procedure, object declaration, or generic instantiation the 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. However, we make an exception for program units (other than subprogram specifications) and bodies, in which the aspect_specification goes before the is. In these cases, the entity could be large and could contain other declarations that also have aspect_specifications, so it is better to put the aspect_specification toward the top of the declaration. (Some aspects - such as Pure - also affect the legality of the contents of a unit, so it would be annoying to only see those after reading the entire unit.) (2) This seems important for consistency. (3) This seems like a good idea for future flexibility. !corrigendum 7.2(2) @drepl @xcode<@fa@b<@ft>@fa< defining_program_unit_name >@b<@ft>@fa< declarative_part [>@b<@ft>@fa< handled_sequence_of_statements] >@b<@ft>@fa< [[parent_unit_name.]identifier]>> @dby @xcode<@fa@b<@ft>@fa< defining_program_unit_name [aspect_specification] >@b<@ft>@fa< declarative_part [>@b<@ft>@fa< handled_sequence_of_statements] >@b<@ft>@fa< [[parent_unit_name.]identifier]>> !corrigendum 9.1(6) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier [>@b<@ft>@fa< declarative_part >@b<@ft>@fa< handled_sequence_of_statements >@b<@ft>@fa< [>@b<@ft>@fa> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [aspect_specification] [>@b<@ft>@fa< declarative_part >@b<@ft>@fa< handled_sequence_of_statements >@b<@ft>@fa< [>@b<@ft>@fa> !corrigendum 9.4(7) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier >@b<@ft>@fa< { protected_operation_item } >@b<@ft>@fa< [>@b<@ft>@fa> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [aspect_specification] >@b<@ft>@fa< { protected_operation_item } >@b<@ft>@fa< [>@b<@ft>@fa> !corrigendum 10.1.3(3/2) @drepl @xcode<@fa@ft<@b>@fa<;>> @dby @xcode<@fa@ft<@b>@fa< [aspect_specification];>> !corrigendum 10.1.3(4) @drepl @xcode<@fa@ft<@b>@fa< defining_identifier >@ft<@b>@fa<;>> @dby @xcode<@fa@ft<@b>@fa< defining_identifier >@ft<@b>@fa< [aspect_specification];>> !corrigendum 10.1.3(5) @drepl @xcode<@fa@ft<@b>@fa< defining_identifier >@ft<@b>@fa<;>> @dby @xcode<@fa@ft<@b>@fa< defining_identifier >@ft<@b>@fa< [aspect_specification];>> !corrigendum 10.1.3(6) @drepl @xcode<@fa@ft<@b>@fa< defining_identifier >@ft<@b>@fa<;>> @dby @xcode<@fa@ft<@b>@fa< defining_identifier >@ft<@b>@fa< [aspect_specification];>> !corrigendum 13.1.1(0) @dinsc Force a conflict; the real text is found in the conflict file. !ACATS test Since there aren't any language-defined aspects allowed in these contexts, there is no way to test that aspects are allowed. (One could check the content of the error messages, but that is not allowed by ACATS testing rules.) So no tests are needed. !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: John Barnes Sent: Friday October 28, 2011 11:35 AM Merci beaucoup JP. Interesting how most people read what they expect to see. **************************************************************** From: Robert Dewar Sent: Friday October 28, 2011 6:52 AM > At the moment that part of the draft rationale says > > The appropriate layout should be obvious. In the case of a structure > that has a specification and body, the aspect specification goes with > the specification before is. The only case where a body can have an > aspect specification is a subprogram without a separate body in which > case the aspect goes before the is of the body. But when something is > all in one piece such as a null procedure, object declaration or > generic instantiation any aspect specification goes at the end of the > declaration; it is then more visible and less likely to interfere with > the layout of the rest of the structure. Seems a clear enough rationale and rule to me! **************************************************************** From: Robert Dewar Sent: Friday October 28, 2011 6:43 AM As an example of preconditions/postconditions in the body consider a memo function. The function is supposed to do two things, properly return the right result (spec post condition), and properly update the memo global data (body post condition). In addition, it checks that its parameters are reasonable (spec precondition), and that the memo data is in ok shape (body precondition). Yes, you can do everything with assertions (even spec pre/post conditions can be modeled this way), but it is cleaner and clearer to be able to use pre/post conditions in both the spec and body. As I say, GNAT already has this capability in full generality, so it doesn't particularly concern me that it is lacking in the standard. **************************************************************** From: Jean-Pierre Rosen Sent: Friday October 28, 2011 7:10 AM > As an example of preconditions/postconditions in the body consider a > memo function. > There are really two ways of seeing things here: 1) Pre/Post are a contract between the client and the provider of the service. In this case, the memo implementation is invisible and pre/post in the body are irrelevant 2) Pre/post are intended to prove correct behaviour of the implementation. Then, body pre/post make sense. My understanding is that the requirement for Ada 2012 was 1). Should we add 2)? TBH, I don't know. Waiting for other voices. **************************************************************** From: Robert Dewar Sent: Friday October 28, 2011 7:26 AM > Should we add 2)? TBH, I don't know. Waiting for other voices. I would think it is a bit late to add 2) at this stage. The question before even considering this would be: if we allow Pre/Post on subprogram bodies, which have separate specs (I don't really care about the silly case of no separate spec), then are there any adverse subtle consequences? If so, I would say drop it, if there are really no problems at all, then it might be worth considering even at this late date (it would be easy to implement in GNAT, we would just remove the arbitrary rule that forbids Pre/Post in bodies :-)) **************************************************************** From: Bob Duff Sent: Friday October 28, 2011 7:30 AM > Should we add 2)? TBH, I don't know. Waiting for other voices. IMHO, we shouldn't be adding new features at this point, especially if some folks don't like them and/or don't see the need. **************************************************************** From: Randy Brukardt Sent: Friday October 28, 2011 12:44 PM > There are really two ways of seeing things here: > 1) Pre/Post are a contract between the client and the provider of the > service. In this case, the memo implementation is invisible and > pre/post in the body are irrelevant > > 2) Pre/post are intended to prove correct behaviour of the > implementation. Then, body pre/post make sense. > > My understanding is that the requirement for Ada 2012 was 1). > > Should we add 2)? TBH, I don't know. Waiting for other voices. I think there is value in using separate (perhaps related) constructs for (1) and (2), so there is no confusion to the clients as to what they can depend on in calls. So I would not want to see any extensions to the existing features. (And it's too late to find Robert's "subtle consequences" with any level of certainty. It might be FUD, but we're close enough to the finish line that FUD is the right approach.) **************************************************************** From: Erhard Ploedereder Sent: Friday October 28, 2011 9:16 AM To sum up my intent: Short of any good arguments still being voiced in favor of aspects on bodies, I would like to shorten the present rule 35/3 An aspect shall not be specified in an aspect_specification given on a subprogram_body that is a completion of another declaration. to An aspect shall not be specified in an aspect_specification given on a subprogram_body. Rationale: Anybody can write a spec if he/she needs aspects. The rule avoids the slightly bothersome syntax permutation on "is..." as discussed earlier. The rule is simple to remember and teach. **************************************************************** From: Robert Dewar Sent: Friday October 28, 2011 9:29 AM I still prefer that we can have aspects on any declaration, since who knows what the requirements are for implementation defined aspects. Do we really want to prohibit an implementation from adding Body_Pre and Body_Post attributes for pre/postconditions in bodies? **************************************************************** From: Tucker Taft Sent: Friday October 28, 2011 9:36 AM I agree we should err on the side of leaving things out at this stage, not adding in new things. **************************************************************** From: Robert Dewar Sent: Friday October 28, 2011 9:42 AM I agree, but to me the "new things" should include any attempts to limit what is now allowed :-) **************************************************************** From: Erhard Ploedereder Sent: Friday October 28, 2011 12:13 PM > Do we really want to prohibit an implementation from adding Body_Pre > and Body_Post attributes for pre/postconditions in bodies? Presently we do prohibit them, if there is a subprogram spec. .. and we allow them if there is no separate spec. which is more or less equal to saying: implementations with specs that are globally visible can have no aspects on their bodies. Only local subprograms can have them. A strange rule indeed. On the question itself: I find invisible Pre- and Postconditions a contradiction in terms. The very reason for having them is to visibly describe behavior. All else can be done with Assertions and suchlike. Pre- and Postconditions are concepts of contract to me, not arbitrary assertion concepts for expressing what is true at the beginning and the end. (I readily agree that there are such additional assertions that are a consequence of implementation, of no concern to the caller, but of concern to the implementer. I just don't believe into heaping them into the pre-/postcondition basket.) **************************************************************** From: Erhard Ploedereder Sent: Friday October 28, 2011 12:21 PM Ok, before someone complains, I forgot separately compiled bodies without spec. But the advice: "you want aspects, you compile it separately" is too bad to even mention ;-) **************************************************************** From: Randy Brukardt Sent: Friday October 28, 2011 12:40 PM > Do we really want to prohibit an implementation from adding Body_Pre > and Body_Post attributes for pre/postconditions in bodies? The original reason we added the capability on subprogram bodies was so that main subprograms don't need a separate specification to define a priority, CPU, deadline, and the like. A separate specification for main subprograms is somewhat weird, and probably would cause a lot of programmers to stick with the pragmas rather than the aspects. But I also agree with Robert's point. If some sort of body postcondition is useful for proofs, then it would make sense to add such an aspect. (It would need to override the current blanket rule for aspects, but of course any aspect can do that, and any impl-def aspect can have whatever rules it likes.) We shouldn't be disallowing that -- we allow almost anything goes. However, that brings up a different question: we don't allow aspects on stubs or other bodies (packages, tasks). Robert's principle here would suggest that we ought to. **************************************************************** From: Robert Dewar Sent: Friday October 28, 2011 3:34 PM > On the question itself: I find invisible Pre- and Postconditions a > contradiction in terms. The very reason for having them is to visibly > describe behavior. All else can be done with Assertions and suchlike. But inconveniently! As I have pointed out several times it is very awkward to use assertions for implementation postconditions, since you don't have 'Result and 'Old, and you have to find all return points, and do a significant bit of rewriting (to deal with not having 'Result). And if you were doing it in your own implementation, you could follow the thought below and add the new aspects and call them something like Assert_On_Entry and Assert_On_Exit. The point is that it is valuable to be *able* to invent such impl defined aspects, rather than forcing implementations to use pragmas instead. (I find myself somewhat inclined to stick with the pragmas in my own GNAT code, since that way I can use the same syntax for specs and bodies, which to me seems prefrable). > Pre- and Postconditions are concepts of contract to me, not arbitrary > assertion concepts for expressing what is true at the beginning and > the end. (I readily agree that there are such additional assertions > that are a consequence of implementation, of no concern to the caller, > but of concern to the implementer. > I just don't believe into heaping them into the pre-/postcondition > basket.) Note that in GNAT, precondition and postcondition pragmas can appear both in the spec and body. We did not invent this out of the blue, a major customer (and major user of Ada) wanted exactly this capability. BTW, that's also a response to Steve's bogus claim [filed as a separate thread below - Editor] that pre/postconditions are ONLY interesting in the context of formal proofs. This same customer was VERY interested in having preconditions/postconditions that work the way they do in Ada (which after all is not that different from the way they are in Eiffel). For an interesting project which attempts to figure out how to combine the two different views of preconditions and postconditions (run time tersts, and aids for formal proving), and in general how to combine testing and proofs, see the hi-lite project: > http://www.open-do.org/projects/hi-lite/ **************************************************************** From: Jean-Pierre Rosen Sent: Saturday October 29, 2011 3:10 PM Here is a suggestion: 1) Keep Pre/Post as intended (the external view contract) 2) State that /language defined/ aspects are not allowed on a body if there is an explicit spec (and presumably, never allowed on separate proper bodies) This leaves an implementation with the possibility of defining its own aspects the way it wants (hint: Implementation_Pre and Implementation_Post for example) Note that for Ada 2019, it would be easy if necessary to change 2) into: Unless otherwise specified, /language defined/ aspects are not allowed etc. **************************************************************** From: Robert Dewar Sent: Saturday October 29, 2011 11:23 PM By the way, in GNAT, our decision on pre/postcondition pragmas isthat if you want spec (caller contract) pre/post conditions, you MUST have a separate spec,I think this is perfectly reasonable, and I see no reason to allow ANY spec aspects on bodies lacking a spec. It just seems plain horrible to me to have different rules for aspects on bodies depending onwhether there is a separate spec. **************************************************************** From: John Barnes Sent: Monday October 31, 2011 3:13 AM >Note that for Ada 2019, it would be easy ..... Count me out. I will be over 81 and in that death and decay phase of life (if not already)! **************************************************************** From: Stephen Michell Sent: Friday October 28, 2011 10:07 AM >> I agree that the contract is one of the reasons. The other reason is >> ... > > Sorry, there is no other reason. Pre and post conditions in Ada 2012 > are purely contract features. Any resemblance to any other feature, > living or dead :-), is purely coincidental. > > Indeed, I would argue that using a contract feature for reasons > unrelated to contracts is likely to be confusing and maybe even > harmful. I understand the need for proof features, but these should > not get mixed with contracts. It's important (if proof is going to be > used on decent sized systems) that separate compilation (and separate > proof) be supported, and for that *only* the contracts matter (because > looking inside of bodies outside of the current unit is not allowed). > Mixing in non-contracts is just going to confuse as to what can and cannot be > depended on. But a contract feature is useless if it cannot be formally shown to be true v **************************************************************** From: Randy Brukardt Sent: Friday October 28, 2011 1:05 PM That is an extreme viewpoint; it seems to say that dynamic constraints (for example) are useless. Dynamic checks have plenty of value. And we decided from the very beginning that Ada's contract features are intended for dynamic checks. Any ability to use them for formal proofs is a happy accident, not something that was intended. I'm willing match your extreme viewpoint with one of my own: proofs that depend on anything *other* than contracts are of little value outside of toy programs. And I don't think complete proofs are worth the effort(*). I want to be able to prove important properties (like absence of exceptions that violate an exception contract) at compile-time, and that means looking in bodies is not allowed. (*) My guess is that if most programmers are faced with the task of defining a complete, provable postcondition for a subprogram, they would end up making a copy of the internal algorithm. That does not add value (especially if the postcondition language is also Ada), it just takes time. In the sorts of subprograms that I often write, there are a few high-level effects that can and should be described in a postcondition, but the details are not worth the effort. Consider the subprogram that adds the declaration of a variable to the symbol table. Something like procedure Add_Var (Decl : in Tree; New_Variable : out Symbol_Ptr); It would make sense that the postcondition include Is_Newly_Added(New_Variable) and Name(New_Variable) = Decl.Id. But trying to describe all of the properties of an object (there are about 30 in Janus/Ada) would just be a waste of time -- the code would end up being a copy of the body of Add_Var. It would add nothing but complexity. So I doubt that there is much value to *complete* formal proofs in a large system. OTOH, there is a lot that can be done with whatever information the programmer puts into the contract, even if the proof is not complete. It's that value (which can directly detect bugs before they happen) that I care about. **************************************************************** From: Stephen Michell Sent: Friday October 28, 2011 1:55 PM We should not be arguing the relative merits of static vs dynamic verification. The point is that the body always knows more about the state of the program than the spec does, and the formal relationship between the preconditions, state, processing and postconditions can be simplified once you can see the "hidden" parts. We need to be able to express these relationships in ways that make verification easier. Artificially prohibiting pre and postconditions on bodies makes our work much harder. **************************************************************** From: Robert Dewar Sent: Saturday October 29, 2011 6:55 AM > We should not be arguing the relative merits of static vs dynamic > verification. I agree, but it was you (Stephen) who raised this issue :-) > The point is that the body always knows more about the state of the > program than the spec does, and the formal relationship between the > preconditions, state, processing and postconditions can be simplified > once you can see the "hidden" parts. We need to be able to express > these relationships in ways that make verification easier. > Artificially prohibiting pre and postconditions on bodies makes our > work much harder. I don't know how artificial that is. But right now, the situation is that in Ada 2012 we regard preconditions and postconditions purely in the Eiffel style, as contracts between the caller and the callee, and obviously both parties must know about a contract, hence Pre and Post conditions are confined to specs. I have agreed that preconditions and postconditions are useful in bodies as well, but three points: a) it is far too late to add this capability to Ada 2012. In particular, if we just add a permission to have Pre/Post on bodies, I would guess that there will be semantic ramifications we do begin to have time to deal with (i.e. this is not just an artificial restriction). b) there is far from a consensus that such an addition is appropriate. At least some feel that it is appropriate to restrict preconditions and postconditions to the "caller contract" model, and object to adding this capability to bodies, regardless of difficulties in definition. c) in practice, the initially widely available implementation of Ada 2012 will allow precondition and postcondition pragmas to appear in bodies, meaning that people can experiment with their use in this context. So I say, let's keep things as they are, and we can revisit this later on if it seems appropriate to do so. **************************************************************** From: Steve Michell Sent: Saturday October 29, 2011 1:27 PM I think that is is the best that we can do for now. **************************************************************** From: Dan Eilers Sent: Saturday October 29, 2011 11:56 AM The argument in c) (which I agree with) that no other vendor finds sufficient merit in the proposed Ada 2012 amendments to actually implement most of then them anytime soon seriously undermines the argument in a) that there is some reason to rush to standardize these amendments. We are due for an Ada 2005 corrigendum soon, to correct the numerous errors in Ada 2005. It was 6 years from publication of Ada 95 to publication of the corrigendum in 2001. 6 years from the publication of Ada 2005 (in 2007) puts the Ada 2005 corrigendum's expected date in 2013. There is however no urgent need for an Amendment anytime soon, especially when all but one vendor is voting with their feet against it, based on their assessments of what the market is interested in. **************************************************************** From: Robert Dewar Sent: Saturday October 29, 2011 1:47 PM I strongly disagree with this. There are numerous reasons to press ahead with the Ada 2012 standard in my view. The perception of continued development and change is important to the continued viability of Ada, and is a big help to our friends who are Ada advocates. Ada 2012 is widely known as such at this stage, and it would be perceieved as unfortunate if it got delayed. I don't see any vital issues that would generate a consensus for a delay, quite the opposite in fact, it seems like most people are of a mind to stick with the schedule. Finally, and most importantly, "assessments of what the market is interested in" are quite strongly related to what in fact the market is interested in. This interest is driven by competition, and the availability of an implementation for Ada 2012 which is available at the same time of the standard will help drive customer demand, and is precisely the factor that is needed to get other vendors moving. For example, I don't think Rational would have announced Ada 2005 if it had not been for their customers expressing interest in Ada 2005, and the fact that those customers had an alternative path to Ada 2005 acted as a useful push. The fact that rational now has Ada 2005 of course heats up the competition, which is certainly fine for rational, fine for its customers, and ultimately fine for everyone, including AdaCore, even if it takes away a marketing advantage. The "numerous errors" in Ada 2005 may concern language lawyers but they don't concern users (or for that matter implementors) to any significant degree. It is much more important to get out the significant new features of Ada 2012 than to tinker around fixing minor problems of no consequence in Ada 2005. **************************************************************** From: Erhard Ploedereder Sent: Saturday October 29, 2011 5:14 AM After an evening of thinking about the problem (occasionally): I agree with Randy whole-heartedly. I have no issue with "body pre-/post-conditions" to reflect implementation properties, as long as they are syntactically distinguished from those that are addressed to the client (and restricted to appear only in the respective constructs - for bi-sexual constructs, both are allowed, of course.) I can envisage two solutions: 1. Add two more aspects with new names that express the idea (obviously the most general solution). 2. The only time this matters is on bodies acting as specs as well. Otherwise the location distinguishes the two kinds of conditions. Hence forbidding aspects on those is a crude but effective mechanism to distinguish the two kinds of pre- and postconditions. And if folks have to spec their Main occasionally, so what ? P.S. Addressed to Steven: Sure, one would like to verify the contractual pre- and postconditions. But this does not depend on the existence of implementation pre- and postconditions, since the very same information can be captured in general Assertions. Whether one calls an assertion a pre- or postcondition does little to alter its semantics. A verification model that presumes that ALL information (including identities) needs to be carried into and across calls with pre- and post-conditions will not scale at all. Admittedly, if you have the all-encompassing pre-/postconditions in mind that you need in a Hoare or Floyd calculus to carry the World-knowledge across calls, then you are right in cramming everything into these predicates. But does that scale at all? My view from 30 years ago and still unchanged is that this model has hindered progress in verification substantially (and unnecessarily). Dijkstra was right about his weakest/strongest pre-/postconditions, which eliminated this restriction a long time ago. You might say: so why not put needed knowledge into pre-/post- at the implementation level, rather than into general assertions? I would not object (anymore) if there were a clear distinction between preconditions whose truth is the responsibility of the caller (i.e., contractual preconditions) and preconditions whose truth is the responsibility of the implementer of a set of connected routines (i.e., implementation invariants). **************************************************************** From: Erhard Ploedereder Sent: Saturday October 29, 2011 7:10 PM > And if you were doing it in your own implementation, you could follow > the thought below and add the new aspects and call them something like > Assert_On_Entry and Assert_On_Exit. The point is that it is valuable > to be *able* to invent such impl defined aspects, rather than forcing > implementations to use pragmas instead. As I said in a later message, I changed my mind about implementation pre/postconditions, but I do want them syntactically distinguished from spec pre/post conditions that need to be established/observed by the caller. Your argument about multiple returns is very convincing. I certainly would be happy with a language-defined Assert_On_Entry/Assert_On_Exit pair for them. **************************************************************** From: Robert Dewar Sent: Tuesday November 1, 2011 9:37 AM Yes, that's probably nicer than reusing pragma Postcondition and pragma Precondition in the body, but now we are stuck with those pragmas in GNAT, perhaps we should allow Assert_On_Entry and Assert_On_Exit as alternative names (or even aspects). Anyway, I think it is too late to try to add this to the Ada2012 definition at this stage??? **************************************************************** From: Erhard Ploedereder Sent: Wednesday November 2, 2011 2:01 PM I don't know. The situation with the placement of the aspects in "bodies as specs" vis-a-vois the "is" has not been resolved. We drifted into this (worthwhile but still peripheral) discussion of spec vs body pre/postconditions and I think additional unintentional nastiness has been discovered (e.g., if you don't use a subprog spec, you can refer to body internals in pre-/postconditions. Exactly the opposite of what good advice should look like.) Maybe both should be a topic at the upcoming meeting. Ed ? **************************************************************** From: Jean-Pierre Rosen Sent: Wednesday November 2, 2011 2:15 PM My understanding is that as soon as the document has been submitted to NB, all comments should come from the NB (but are still doable). Therefore, we should discuss remaining issues at the ARG meeting, but any change we decide has to come from some NB (there are enough of us involved with their NB to spread the "comments" over various nations) **************************************************************** From: Robert Dewar Sent: Wednesday November 2, 2011 2:20 PM > We drifted into this (worthwhile but still peripheral) discussion of > spec vs body pre/postconditions and I think additional unintentional > nastiness has been discovered (e.g., if you don't use a subprog spec, > you can refer to body internals in pre-/postconditions. > Exactly the opposite of what good advice should look like.) I don't think that's the case at all, I don't think these pre and post have any more visibility than the caller does. **************************************************************** From: Edmond Schonberg Sent: Wednesday November 2, 2011 2:48 PM We should certainly come to a consensus on this in Denver. It will be on the agenda. **************************************************************** From: Randy Brukardt Sent: Wednesday November 2, 2011 5:09 PM Way ahead of you. Created and posted an AI last night. **************************************************************** From: Erhard Ploedereder Sent: Wednesday November 2, 2011 7:10 PM > I don't think that's the case at all, I don't think these pre and post > have any more visibility than the caller does. As I wrote my mail, I started thinking about that, too. Presumably, at a minimum, implementation aspects/pragmas would have visibility of private type completions that the aspects on the spec cannot see. Anything else? Stephen? **************************************************************** From: Robert Dewar Sent: Wednesday November 2, 2011 7:05 PM Well we are talking not about implementation aspects Post and Pre etc predefined in the language, but rather the use of these on the body when there is no spec. I agree it's unclear what they can see. I really MUCH prefer we just ban Pre/Post etc aspects on a subprogram body period. If people want these aspects they MUST write a spec, that seems a perfectly reasonable rule. Bodies with no specs are warts, and we should not waste time on additional makeup to cover them up! **************************************************************** From: Erhard Ploedereder Sent: Wednesday November 2, 2011 7:58 PM That is exactly were I was standing a few days ago - and it is of course not the state of Draft 14. Then came some Robert D., who made a convincing argument that there should be Pre/Post on bodies as well ("multiple returns", interaction with exceptions, etc. etc.). An evil twin? :-) Admittedly you argued for impl-defined ones, because you already have them in the form of pragmas. But if they are needed, they are not precarious to add to the language itself, as long as the two kinds are kept well separated. **************************************************************** From: Robert Dewar Sent: Wednesday November 2, 2011 8:10 PM I was NOT arguing for adding these to the language, merely for keeping the possibility of adding impl-defined ones. We have two separate issues here and you are I think confusing them. For contract Pre/Post aspects, normally on the spec, because they must be visible to the caller, are we allowed to park them on the body when there is no spec? The definition currently says yes, I think this is a confusing mistake, which should be rectified by the simple method of saying NO to this quesation. Totally separate issuee, should there be some kind of Pre/Post capability on bodies? Maybe yes, but robert thinks a) it is too late to stick that in the standard b) we should allow impl defined aspects on bodies so that implementors can add this capability if they like. **************************************************************** From: Randy Brukardt Sent: Monday November 7, 2011 6:01 PM ... > For contract Pre/Post aspects, normally on the spec, because they must > be visible to the caller, are we allowed to park them on the body when > there is no spec? The definition currently says yes, I think this is a > confusing mistake, which should be rectified by the simple method of > saying NO to this quesation. We allow aspects on subprogram bodies so that aspects like Priority can be specified on bodies without requiring a separate specification. (That would be weird for a main subprogram, which is the only kind of subprogram that can have Priority.) We use the same rules for all aspects, but of course there is no requirement to do that. But I have to admit, I don't see any problem here. If you put Pre on a body (that has no spec), it is true that the precondition can see private declarations. But that's not a problem, since any caller *also* has to be able to see those declarations (since if they can see the subprogram body, they can also see the private declarations). So it is fine to allow such in the preconditions. If someone later adds a separate specification, the precondition would have to move and be changed, but that seems like a different situation. So I don't think we need a change here. > Totally separate issuee, should there be some kind of Pre/Post > capability on bodies? > > Maybe yes, but robert thinks > > a) it is too late to stick that in the standard Agreed. > b) we should allow impl defined aspects on bodies so that implementors > can add this capability if they like. That's already true, as any aspect (including language-defined ones) is allowed to invent its own rules, and surely that's the case for implementation-defined aspects. The only open questions [related to that] that I know of is (1) should we allow aspect_specifications on stubs? Presumably with similar rules to bodies (2) should we allow aspect_specifications on package/task/protected bodies, only for implementation-defined aspects. I lean toward "Yes" on both of these questions, especially as we already did the latter for renames and generic formal parameters (no language-defined aspects, but the clause is allowed). Don't see much reason for these other things to be different. **************************************************************** From: Robert Dewar Sent: Monday November 7, 2011 6:06 PM > But I have to admit, I don't see any problem here. If you put Pre on a > body (that has no spec), it is true that the precondition can see > private declarations. But that's not a problem, since any caller > *also* has to be able to see those declarations (since if they can see > the subprogram body, they can also see the private declarations). So > it is fine to allow such in the preconditions. OK > If someone later adds a separate specification, the precondition would > have to move and be changed, but that seems like a different situation. > > So I don't think we need a change here. OK, not a big deal for me >> Totally separate issuee, should there be some kind of Pre/Post >> capability on bodies? >> >> Maybe yes, but robert thinks >> >> a) it is too late to stick that in the standard > > Agreed. > >> b) we should allow impl defined aspects on bodies so that >> implementors can add this capability if they like. > > That's already true, as any aspect (including language-defined ones) > is allowed to invent its own rules, and surely that's the case for > implementation-defined aspects. OK, was just reacting to one suggestion of taking this away > The only open questions [related to that] that I know of is (1) should > we allow aspect_specifications on stubs? Presumably with similar rules > to bodies (2) should we allow aspect_specifications on > package/task/protected bodies, only for implementation-defined > aspects. I lean toward "Yes" on both of these questions, especially as > we already did the latter for renames and generic formal parameters > (no language-defined aspects, but the clause is allowed). Don't see much > reason for these other things to be different. I agree with randy on this ****************************************************************