!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) @dinsc 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. ****************************************************************