Version 1.5 of ai12s/ai12-0169-1.txt
!standard 9.5.2(5) 15-07-08 AI12-0169-1/02
!class binding interpretation 15-06-17
!status Amendment 1-2012 16-02-29
!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