Version 1.4 of ai12s/ai12-0169-1.txt

Unformatted version of ai12s/ai12-0169-1.txt version 1.4
Other versions for file ai12s/ai12-0169-1.txt

!standard 9.5.2(5)          15-07-08 AI12-0169-1/02
!class binding interpretation 15-06-17
!status WG9 Approved 15-10-16
!status ARG Approved 7-0-2 15-06-26
!status work item 15-06-17
!status received 15-06-05
!priority Low
!difficulty Easy
!qualifier Omission
!subject Aspect specifications for entry bodies
!summary
Aspect specifications are allowed on entry bodies (for implementation-defined aspects).
!question
Ada syntax allows an aspect_specification to occur in 37 different contexts, but an entry_body isn't one of them.
This seems like it was just an oversight. The permission for implementation-defined aspects doesn't allow putting aspect_specifications in new places. We need an implementation-defined aspect for SPARK on entry bodies.
Should this be changed? (Yes.)
!recommendation
(See Summary.)
!wording
Replace 9.5.2(5) by:
entry_body ::= entry defining_identifier entry_body_formal_part [aspect_specification] entry_barrier is declarative_part begin handled_sequence_of_statements end [entry_identifier];
[Editor's note: The only change here is the addition of an optional aspect_specification. We never describe syntax changes with insertion and deletion brackets, because those are legal syntax descriptors and it is impossible to tell which is meant.]
!discussion
Toward the end of the Ada 2012 effort, we decided to add aspect_specification to all bodies, as we thought that it might be useful to specify implementation-defined aspects there. However, we failed to do that for entry bodies; that seems like a clear oversight.
The location of the aspect_specification is as proposed. This is an inconsistent location; for all other bodies, the aspect specification goes directly before the IS.
There a couple of reasons for this: reasonable aspects may affect the entry_barrier, so it seemed appropriate for it to precede the entry barrier. And there isn't really a definition of "header" -- one could see the entry_barrier as part of the body rather than the specification. After all, it doesn't appear as part of the entry declaration.
The AI author doesn't buy this; this aspect_specification will be little-used and putting it in a non-standard place will be a continual annoyance (just as having the aspect_specification after "is abstract" and "is null" is an annoyance, because one always puts it before the "is" and then gets a syntax error, then looks up the syntax again, then moves it to the right place. Repeat ad-nausem).
In the e-mail, there also was a suggestion aspects are better first because the entry barrier might be very long ("running on several lines"). But of course some aspects could also be "very long" (that's certainly true of Pre and Post), and arguably it would be best to put these things in order of importance. That is, having the barrier (which is critical to the Ada semantics) after a bunch of implementation-defined glop (which is not part of the Ada semantics) seems like an inversion.
The full ARG was split exactly down the middle on this, and as we have to do something, we left the original proposal as it was (it was reputed to be better for SPARK this way).
!ASIS
No ASIS effect.
!ACATS test
No ACATS test is possible until/unless there is a language defined aspect allowed on entry bodies.
!appendix

From: Steve Baird
Sent: Thursday, June 4, 2015  4:18 PM

Hopefully this one is a simple, non-controversial change.

Ada syntax allows an aspect_specification to occur in
37 different contexts, but an entry_body isn't one of them.

This seems like it was just an oversight and now SPARK needs this capability.

It does not seem that the 13.1.1 permissions

   The aspect_specification for an implementation-defined aspect may use
   an implementation-defined syntax for the aspect_definition, and may
   follow implementation-defined legality and semantics rules.

help in this case.

So the following one-line grammar change is proposed:

!wording

Modify 9.5.2(5)

   entry_body ::=
       ENTRY defining_identifier entry_body_formal_part
       { [aspect_specification] }
       entry_barrier IS
       declarative_part
       begin
         handled_sequence_of_statements
       end [entry_identifier];

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

From: Jean-Pierre Rosen
Sent: Friday, June 5, 2015  3:42 AM

Shouldn't the aspect_specification be after the entry_barrier?

Normally, aspects are stuck at the end, here it would appear in the middle
of the header.

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

From: Tucker Taft
Sent: Friday, June 5, 2015  7:29 AM

We debated that.  At least in our use, the aspects may affect the
entry_barrier, so it seemed appropriate for it to precede the entry barrier.
And there isn't really a definition of "header" -- one could see the
entry_barrier as part of the body rather than the specification.  After all,
it doesn't appear as part of the entry declaration.

I agree it isn't totally obvious, and either could work.

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

From: Tullio Vardanega
Sent: Friday, June 5, 2015  7:51 AM

If, as it seems to be the intent, the aspect should affect the entry barrier,
then it should be logical that the aspect spec precedes the barrier spec.

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

From: Tucker Taft
Sent: Friday, June 5, 2015  7:59 AM

I might add that in some of my uses of entry barriers, they can be very
complex, running on for several lines.  It feels like it would be better for
aspect specifications to precede all of that.

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


Questions? Ask the ACAA Technical Agent