!standard 6.1.1(30/3) 15-11-19 AI12-0143-1/03 !standard 9.5.4(5/3) !class Amendment 15-01-28 !status ARG Approved 5-0-2 15-10-18 !status Promising (9-0-0) 15-01-28 !status work item 14-12-04 !status received 14-11-12 !priority Low !difficulty Easy !subject Using an entry index of a family in a precondition !summary Add the E'Index attribute for preconditions and postconditions. !problem Parameters of an entry can be used within preconditions and postconditions. However, the entry family index of an entry call does not have a name in the entry specification, and thus cannot be used in preconditions or postconditions. This value serves a role similar to that of parameters, and it's weird not to be able to use it. !proposal (See Wording.) !wording Add after 6.1.1(30/3): For a prefix E that denotes an entry declaration of an entry family, the following attribute is defined: E'Index Within a precondition or postcondition expression for entry family E, denotes the value of the entry index for the call of E. The nominal subtype of this attribute is the entry index subtype. [Editor's note: We don't mention the type of the attribute, because it is "obviously" the type of the nominal subtype.] Use of this attribute is allowed only within a precondition or postcondition expression for E. Modify 9.5.4(5.4/4) (added by AI12-0090-1 in the Corrigendum): The requeue target shall not have an applicable specific or class-wide postcondition {that}[which] includes an Old {or Index} attribute_reference. !discussion We define this attribute only within preconditions and postconditions as it can only be meaningful during an entry call. Inside of an entry_body, it already has a name, and it has to be known for an accept_statement. So there is no need for the attribute outside of preconditions and postconditions. Note that the correct terminology is "entry index" of an "entry family" (see 9.5.2); it is not "family index" or even "entry family index". The addition to the requeue rule is for the same reason that we ban 'Old in that rule (see AI12-0090-1) - the parameters (and family index) for the requeue target can be different than that for the original entry call. In particular, consider requeuing to the same entry with a different family index; in such a case, the postcondition would conform, but the expression evaluated on completion of the target entry would not necessarily imply that the original postcondition was true. !ASIS Add the following value to the type Attribute_Kinds: An_Index_Attribute !ACATS test We need an ACATS C-Test to test the new attribute. !appendix From: Randy Brukardt Sent: Wednesday, November 12, 2014 10:44 PM In the minutes of the most recent meeting, I have: Steve Michell notes that one can use the entry family index in a postcondition. Since you can internally requeue to a different entry family, that could cause the postcondition to be a lie. Do we care? (We're not trying to fix all such cases.) Tucker suggests that the postcondition cannot depend on an entry index. So add that to the 'Old rule. I started trying to add entry family index to the rule, and I went to look up the actual name for the concept. And I noticed something interesting. The syntax for an entry declaration is (this used for both task entries and protected entries): entry_declaration ::= [overriding_indicator] entry defining_identifier [(discrete_subtype_definition)] parameter_profile [aspect_specification]; The thing to note here is that the entry family does not have a name in the specification. (It does have a name in an entry_body, but that clearly isn't visible to a postcondition.) As such, it should be clear that Steve was wrong, one CANNOT write a postcondition (or precondition) that depends on the entry family index. So we don't need an extra rule in AI12-0090-1. OTOH, it seems to be rather limiting not to be able to reference the family in pre- and postconditions. Perhaps we want to come up with a way to do that? (That's probably not a Corrigendum fix, unless we decide to invent an attribute for it.) If we did that, THEN we'd need a rule for requeue. Am I right here? Or did I miss something? **************************************************************** From: Tucker Taft Sent: Thursday, November 13, 2014 7:27 AM > ... OTOH, it seems to rather limiting not to be able to reference the > family in > pre- and postconditions. Perhaps we want to come up with a way to do that? > (That's probably not a Corrigendum fix, unless we decide to invent an > attribute for it.) If we did that, THEN we'd need a rule for requeue. > > Am I right here? Or did I miss something? No, I think you found something. Hard to get excited about entry families, but they do show up in places like the Burns and Wellings book to implement things like resource managers, so using the entry family index in a pre- or postcondition would be quite reasonable. I think it should probably be handled by an attribute rather than a syntax change, something analogous to 'Caller, like 'Index, but it doesn't seem high enough priority to make it into this Corrigendum. **************************************************************** From: Randy Brukardt Sent: Thursday, November 13, 2014 4:53 PM Sounds like another AI. It would be easy enough to write up a proposal for an 'Index attribute, and if time permits at our January phone meeting, we could take a look at it. I'd have one question, though. Should it be defined like 'Old (only for preconditions or postconditions) or something more general? It would make sense in accept statements as well as preconditions and postconditions for an entry, but of course allowing it in accept statements complicates the definition. (In entry bodies, it has a name so there's no real value to allowing it, but no huge harm either.) We surely don't want to allow it everywhere, because the value wouldn't be well-defined unless it is associated with a particular entry call. I guess I'd lean toward defining it with 'Old and 'Result for ease of definition (there's an obvious place for it there, and there's no special scoping issues there - it would be allowed IFF the pre/post is on an entry with a family). Thoughts? **************************************************************** From: Tucker Taft Sent: Thursday, November 13, 2014 10:25 PM I would say we should definitely restrict it to pre/postconditions. We could relax it later, I suppose, if there were some real demand for it. **************************************************************** From: Jean-Pierre Rosen Sent: Friday, November 14, 2014 2:37 AM > I'd have one question, though. Should it be defined like 'Old (only > for preconditions or postconditions) or something more general? It > would make sense in accept statements as well as preconditions and > postconditions for an entry, but of course allowing it in accept > statements complicates the definition. (In entry bodies, it has a name > so there's no real value to allowing it, but no huge harm either.) Even in entry bodies, the entry index is given by an expression, but it is easy to use a variable if the value is needed in the entry body - and it's probably what people are currently doing if there is a need for that. I don't see much value in allowing 'Index outside Pre/Post. **************************************************************** From: Erhard Ploedereder Sent: Saturday, November 15, 2014 6:00 PM Restrict it to Pre- and Postconditions. If you make it more general, you need to answer the question what it means to call Family'Index outside some accept statement for Family -- namely nothing sensible. 'Index as an attribute is quirky, because it is an attribute of a call on the entry, not of the entry itself (as 'Count is, for example). ****************************************************************