Version 1.7 of ai12s/ai12-0143-1.txt

Unformatted version of ai12s/ai12-0143-1.txt version 1.7
Other versions for file ai12s/ai12-0143-1.txt

!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 Amendment 1-2012 16-02-29
!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 (see 9.5.2), 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.
!corrigendum 6.1.1(30/3)
Insert after the paragraph:
Use of this attribute is allowed only within a postcondition expression for F.
the new paragraphs:
For a prefix E that denotes an entry declaration of an entry family (see 9.5.2), 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.
Use of this attribute is allowed only within a precondition or postcondition expression for E.
!corrigendum 9.5.4(5.4/4)
Replace the paragraph:
The requeue target shall not have an applicable specific or class-wide postcondition which includes an Old attribute_reference.
by:
The requeue target shall not have an applicable specific or class-wide postcondition that includes an Old or Index attribute_reference.
!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).

****************************************************************

Questions? Ask the ACAA Technical Agent