Version 1.2 of ai12s/ai12-0332-1.txt

Unformatted version of ai12s/ai12-0332-1.txt version 1.2
Other versions for file ai12s/ai12-0332-1.txt

!standard 7.3.3(9/5)          19-05-09 AI12-0332-1/02
!class Amendment 19-05-07
!status Amendment 1-2012 19-05-09
!status ARG Approved 9-0-0 19-05-09
!status work item 19-05-07
!status received 19-04-26
!priority Low
!difficulty Easy
!subject Implementation Permission for Default_Initial_Condition
!summary
An implementation can allow other forms of default initial condition.
!problem
Default_Initial_Condition was originally a SPARK construct, now available in Ada. However, the original SPARK construct allows some additional forms beyond those allowed for Ada. This means that some SPARK programs which were legal Ada 2012 programs will become illegal as Ada 2020 programs. (Remember that an implementation is not allowed to extend language-defined aspects and attributes unless a permission is given to that effect.)
!proposal
(See Summary.)
!wording
Add after 7.3.3(9/5):
Implementation Permissions
Implementations may extend the syntax or semantics of the Default_Initial_Condition aspect in an implementation-defined manner.
!discussion
This permission might cause a portability issue, but it is relatively easy to restrict oneself to Boolean expressions (which will always work on any correct implementation).
!corrigendum 7.3.3(0)
Insert new clause:
We just need to force a conflict; the actual change is in the conflict file.
!ASIS
No change to ASIS is needed.
!ACATS test
No ACATS tests are needed for this permission (permissions are not generally testable). Arguably, B-Tests for this feature may need modification (so that they allow a construct that would normally be illegal), but in general we will wait for an implementer to complain before changing any such tests.
!appendix

From: Steve Baird
Sent: Friday, April 26, 2019  2:26 PM

Suppose SPARK defines some new Aspect (or attribute, or pragma), which 
is later incorporated (possibly with some changes) into Ada.

Initially (i.e., before the construct becomes part of the Ada standard),
there is no problem. From Ada's perspective, this is just another
implementation-defined construct of the sort that is explicitly
permitted by, for example, Ada RM 13.1.1:
    Implementations may support implementation-defined aspects.

 From SPARK's perspective, the construct is part of the (SPARK)
language.

But a SPARK program is supposed to be compilable as an Ada program.

This apparent conflict is resolved by saying that a SPARK program
should be compilable as an Ada program when using an Ada compiler that
supports the appropriate set of implementation-defined aspects,
attributes, and pragmas.

This is described in the SPARK RM:
   SPARK 2014 may make use of certain aspects, attributes and pragmas
   which are not defined in the Ada 2012 reference manual. Ada 2012
   explicitly permits implementations to provide implementation-defined
   aspects, attributes and pragmas. If a SPARK 2014 program uses one of
   these aspects (e.g., Global), or attributes (e.g., Update) then it can
   only be compiled and executed by an implementation which supports the
   construct in a way consistent with the definition given here in the
   SPARK 2014 reference manual.

For more on this, see
 
docs.adacore.com/live/wave/spark2014/html/spark2014_rm/introduction.html#dynamic-semantics-of-spark-programs

So far, no problem.

So suppose the SPARK construct is added to the Ada standard, but
with some (typically minor) changes. We don't want to cause SPARK
programs which were legal Ada 2012 programs to become illegal as
Ada 2020 programs.

Tuck recently proposed adding an implementation permission to address
this situation in the case of the Global aspect.

Another such situation arises in the case of the 
Default_Initial_Condition aspect and I think we need an analogous
implementation permission.

Spark allows
    type T is private with Default_Initial_Condition => null;

The precise meaning of "Default_Initial_Condition => null" in SPARK is
unimportant for the Ada. Roughly speaking, it means that default
initialization of an object of the given type leaves the object
uninitialized.For details, see
 
docs.adacore.com/live/wave/spark2014/html/spark2014_rm/packages.html#default-initial-condition-aspects

The point is that we want an implementation permission which allows it
despite the (correct and desirable) RM 7.3.3 rule that the expected type
for a default initial condition expression is any boolean type.

Perhaps append an "Implementation Permissions" section to the end of 
7.3.3 which contains

    Implementations may choose to accept a Default_Initial_Condition
    aspect specification which would not be allowed by the rules
    given in this section (e.g., one specifying an expression whose type
    is not a Boolean type). The (static and dynamic) semantics
    associated with any such aspect specification are implementation
    defined.

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

From: Randy Brukardt
Sent: Monday, May 6, 2019  8:08 PM

...
> Tuck recently proposed adding an implementation permission to address 
> this situation in the case of the Global aspect.
> 
> Another such situation arises in the case of the 
> Default_Initial_Condition aspect and I think we need an analogous 
> implementation permission.

You probably didn't need to write a small novel to justify this suggestion.
:-) It seems obvious enough.

> Spark allows
>     type T is private with Default_Initial_Condition => null;
> 
> The precise meaning of "Default_Initial_Condition => null" in SPARK is 
> unimportant for the Ada. Roughly speaking, it means that default 
> initialization of an object of the given type leaves the object 
> uninitialized.For details, see
>  
> docs.adacore.com/live/wave/spark2014/html/spark2014_rm/package
> s.html#default-initial-condition-aspects
> 
> The point is that we want an implementation permission which allows it 
> despite the (correct and desirable) RM 7.3.3 rule that the expected 
> type for a default initial condition expression is any boolean type.
> 
> Perhaps append an "Implementation Permissions" section to the end of
> 7.3.3 which contains
> 
>     Implementations may choose to accept a Default_Initial_Condition
>     aspect specification which would not be allowed by the rules
>     given in this section (e.g., one specifying an expression whose type
>     is not a Boolean type). The (static and dynamic) semantics
>     associated with any such aspect specification are implementation
>     defined.

This is fine, other than that we don't use "e.g.". That should be "for
instance".

Do you want me to write up a simple AI with this change?? (I know better than 
to assume I'll get one from you even if I beg. ;-)

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

From: Steve Baird
Sent: Tuesday, May 7, 2019  1:47 PM

I accept your generous offer.

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


Questions? Ask the ACAA Technical Agent