!standard 7.3.3(0) 18-04-26 AI12-0265-1/03 !standard 1.1.3(17.1/5) !standard 11.4.2(23.2/5) !standard 11.4.2(23.3/5) !class Amendment 18-03-28 !status Amendment 1-2012 18-04-04 !status WG9 Approved 16-06-22 !status ARG Approved 7-0-2 18-04-02 !status work item 18-03-28 !status received 18-03-20 !priority Low !difficulty Easy !subject Default_Initial_Condition for types !summary Define a new contract aspect, Default_Initial_Condition. !problem SPARK allows users to specify a Default_Initial_Condition aspect for a type; it is essentially a postcondition for the type's default initialization. It is a boolean expression (typically involving the current instance of the type) which is checked after default initialization of an object (that is, immediately after the places where Initialize would be called in the case of a controlled type). Such a condition is useful for setting the initial conditions of an object. One specific case where it would be useful is for specifying the initial state of any stable properties of the type. Otherwise, analysis could determine the values of the properties on all paths except those that start with default-initialized objects. !proposal (See Summary.) !wording Add a new subclause: 7.3.3 Default Initial Conditions For a private type or private extension, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1): Default_Initial_Condition This aspect shall be specified by an expression, called a default initial condition expression. Default_Initial_Condition may be specified on a private_type_declaration or a private_extension_declaration. Name Resolution The expected type for a default initial condition expression is any boolean type. Legality Rules The Default_Initial_Condition aspect shall not be specified for a type whose partial view has unknown discriminants [, whether explicitly declared or inherited]. Static Semantics If the Default_Initial_Condition aspect is specified for a type T, then the default initial condition expression applies to T and to all descendants of T. Dynamic Semantics If one or more default initial condition expressions apply to a type T, then a default initial condition check is performed after successful default initialization of an object of type T by default (see 3.3.1). In the case of a controlled type, the check is performed after the call to the type's Initialize procedure (see 7.6). If performing checks is required by the Default_Initial_Condition assertion policy (see 11.4.2) in effect at the point of the corresponding aspect specification applicable to a given type, then the respective default initial condition expression is considered enabled. The default initial condition check consists of the evaluation of each enabled default initial condition expression that applies to T. These evaluations, if there are more than one, are performed in an arbitrary order. If any of these evaluate to False, Assertions.Assertion_Error is raised at the point of the object initialization. ---- Modify 1.1.3(17.1/5): For an implementation that conforms to this Standard, the implementation of a language-defined unit shall abide by all postconditions{, default initial conditions,} and type invariants specified for the unit by this International Standard (see 11.4.2). Modify 11.4.2(1.1/3): Assert pragmas, subtype predicates (see 3.2.4), preconditions and postconditions (see 6.1.1), [and ]type invariants (see 7.3.2){, and default initial conditions (see 7.3.3)} are collectively referred to as assertions; Modify 11.4.2(9/3): The assertion_aspect_mark of a pragma Assertion_Policy shall be one of Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class, Post, Post'Class, Type_Invariant, Type_Invariant'Class, {Default_Initial_Condition, }or some implementation defined aspect_mark. The policy_identifier shall be either Check, Ignore, or some implementation-defined identifier. Modify 11.4.2(23.2/5): Any postcondition expression{,}[ or] type invariant expression {, or default initial condition expression} occurring in the specification of a language-defined unit is enabled (see 6.1.1, [and ]7.3.2{, and 7.3.3}). Modify 11.4.2(23.3/5): The evaluation of any such postcondition{,} [or ]type invariant {, or default initial condition} expression shall ... !discussion If one imagines that the default initialization of the object is described by a function D_I, this contract describes the postcondition of that (hypothetical) function. In this postcondition, the current instance of the type takes the place of D_I'Result, and the only parameters could be the bounds or discriminants of the type (so 'Old is not useful). Therefore, we don't need any of those special capabilities in Default_Initial_Condition as would do in real postconditions. The comparison to postconditions answers various other questions: the contract shouldn't be hidden, we don't need a class-wide version, inheritance is mandatory, and so on. Some of these points need some explanation: we don't need a class-wide version of this aspect because a default-initialized object of a class-wide type is illegal (class-wide types are always indefinite). As such, the specific type is always known and there is no equivalent of a dispatching call to support. However, we require inheritance of these conditions. That's because Ada doesn't allow changing the default initialization when a type is derived or extended. As such, the original condition has to remain true. Additional conditions can be defined, but these are "and"ed (like Postconditions). !example package Sets is type Set is private with Default_Initial_Condition => Is_Empty (Set); function Is_Empty (S : Set) return Boolean; ... end Sets; !corrigendum 1.1.3(17/3) @dinsa An implementation conforming to this International Standard may provide additional aspects, attributes, library units, and pragmas. However, it shall not provide any aspect, attribute, library unit, or pragma having the same name as an aspect, attribute, library unit, or pragma (respectively) specified in a Specialized Needs Annex unless the provided construct is either as specified in the Specialized Needs Annex or is more limited in capability than that required by the Annex. A program that attempts to use an unsupported capability of an Annex shall either be identified by the implementation before run time or shall raise an exception at run time. @dinst For an implementation that conforms to this Standard, the implementation of a language-defined unit shall abide by all postconditions, type invariants, and default initial conditions specified for the unit by this International Standard (see 11.4.2). !corrigendum 7.3.3(0) @dinsc For a private type or private extension, the following language-defined aspect may be specified with an @fa (see 13.1.1): @xhang<@xtermThis aspect shall be specified by an expression, called a @i. Default_Initial_Condition may be specified on a @fa or a @fa.> @s8<@i> The expected type for a default initial condition expression is any boolean type. @s8<@i> The Default_Initial_Condition aspect shall not be specified for a type whose partial view has unknown discriminants, whether explicitly declared or inherited. @s8<@i> If the Default_Initial_Condition aspect is specified for a type T, then the default initial condition expression applies to T and to all descendants of T. @s8<@i> If one or more default initial condition expressions apply to a type T, then a default initial condition check is performed after successful default initialization of an object of type T by default (see 3.3.1). In the case of a controlled type, the check is performed after the call to the type's Initialize procedure (see 7.6). If performing checks is required by the Default_Initial_Condition assertion policy (see 11.4.2) in effect at the point of the corresponding @fa applicable to a given type, then the respective default initial condition expression is considered enabled. The default initial condition check consists of the evaluation of each enabled default initial condition expression that applies to T. These evaluations, if there are more than one, are performed in an arbitrary order. If any of these evaluate to False, Assertions.Assertion_Error is raised at the point of the object initialization. !corrigendum 11.4.2(1.1/3) @drepl Assert pragmas, subtype predicates (see 3.2.4), preconditions and postconditions (see 6.1.1), and type invariants (see 7.3.2) are collectively referred to as @i; their boolean expressions are referred to as @i. @dby Assert pragmas, subtype predicates (see 3.2.4), preconditions and postconditions (see 6.1.1), type invariants (see 7.3.2), and default initial conditions (see 7.3.3) are collectively referred to as @i; their boolean expressions are referred to as @i. !corrigendum 11.4.2(9/3) @drepl The @i@fa of a @fa Assertion_Policy shall be one of Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class, Post, Post'Class, Type_Invariant, Type_Invariant'Class, or some implementation defined @fa. The @i@fa shall be either Check, Ignore, or some implementation-defined @fa. @dby The @i@fa of a @fa Assertion_Policy shall be one of Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class, Post, Post'Class, Type_Invariant, Type_Invariant'Class, Default_Initial_Condition, or some implementation defined @fa. The @i@fa shall be either Check, Ignore, or some implementation-defined @fa. !corrigendum 11.4.2(23.1/3) @dinsa It is a bounded error to invoke a potentially blocking operation (see 9.5.1) during the evaluation of an assertion expression associated with a call on, or return from, a protected operation. If the bounded error is detected, Program_Error is raised. If not detected, execution proceeds normally, but if it is invoked within a protected action, it might result in deadlock or a (nested) protected action. @dinss @s8<@i> Any postcondition expression, type invariant expression, or default initial condition expression occurring in the specification of a language-defined unit is enabled (see 6.1.1, 7.3.2, and 7.3.3). The evaluation of any such postcondition, type invariant, or default initial condition expression shall either yield True or propagate an exception from a @fa that appears within the assertion expression. !ASIS [Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.] !ACATS test ACATS B- and C-Tests are needed to check that the new capabilities are supported. !appendix From: Steve Baird Sent: Friday, March 16, 2018 1:00 AM SPARK allows users to specify a Default_Initial_Condition aspect for a type; it is essentially a postcondition for the type's default initialization. It is a boolean expression (typically involving the current instance of the type) which is checked after default initialization of an object (i.e., immediately after the places where Initialize would be called in the case of a controlled type). For example, package Sets is type Set is private with Default_Initial_Condition => Is_Empty (Set); function Is_Empty (S : Set) return Boolean; ... end; This aspect has the usual interactions with pragma Assertion_Policy. Presumably D_I_C and Preelaborable_Initialization are mutually exclusive. I've wanted this feature in Ada many times, most recently in working on the Big_Nums spec. For details of how it is defined in SPARK, see docs.adacore.com/spark2014-docs/html/lrm/packages.html#default-initial-condition -aspects although Ada might not want to follow that definition in every detail (e.g., Spark allows "Default_Initial_Condition => null" and gives that construct a special meaning). Should we define this aspect in Ada? SPARK also allows specifying an Initial_Condition aspect for a package, which acts as the postcondition for a package's elaboration. It is roughly equivalent to a pragma Assert occurring at the end of the elaboration of the package body, but it textually occurs in the package spec. For example, package Roswell with Initial_Condition => UFO_Sightings = 0 is function UFO_Sightings return Natural; end; This one seems less important for Ada than Default_Initial_Condition, but we still might want to consider it. For details of how this aspect is defined in SPARK, see docs.adacore.com/spark2014-docs/html/lrm/packages.html#initial-condition-aspects **************************************************************** From: Randy Brukardt Sent: Monday, March 19, 2018 7:41 PM ... > This aspect has the usual interactions with pragma Assertion_Policy. > Presumably D_I_C and Preelaborable_Initialization are mutually > exclusive. Why this last? That seems to prevent using proper contracts for types in pure and preelaborable packages, which seems strange, as we always try to make language defined packages one or the other. The aspect would be very useful with the Stable_Properties aspect, as it could be used to set the initial conditions for those properties (necessary to enable optimization/proof involving default initialized objects). But the containers (for instance), which use various Stable_Properties, declare both the container and the cursor with Preelaborable_Initialization. > I've wanted this feature in Ada many times, most recently in working > on the Big_Nums spec. As noted above, it seems that it would be valuable for the containers. > For details of how it is defined in SPARK, see > docs.adacore.com/spark2014-docs/html/lrm/packages.html#default > -initial-condition-aspects > although Ada might not want to follow that definition in every detail > (e.g., Spark allows "Default_Initial_Condition => null" > and gives that construct a special meaning). > > Should we define this aspect in Ada? I think so. > SPARK also allows specifying an Initial_Condition aspect for a > package, which acts as the postcondition for a package's elaboration. > It is roughly equivalent to a pragma Assert occurring at the end of > the elaboration of the package body, but it textually occurs in the > package spec. > > For example, > > package Roswell > with Initial_Condition => UFO_Sightings = 0 > is > function UFO_Sightings return Natural; > end; > > This one seems less important for Ada than Default_Initial_Condition, > but we still might want to consider it. > > For details of how this aspect is defined in SPARK, see > docs.adacore.com/spark2014-docs/html/lrm/packages.html#initial > -condition-aspects There's a lot of possible contracts that we could consider (loop invariants, for one) that are more important than this one. I'd rather not muck up a valuable contract (Default_Initial_Condition) by mixing it up with something with a similar name but much less utility. (Ideally, packages don't have externally visible state, so one couldn't say anything useful in such a contract.) **************************************************************** From: Randy Brukardt Sent: Monday, March 19, 2018 8:08 PM > Why this last? That seems to prevent using proper contracts for types > in pure and preelaborable packages, which seems strange, as we always > try to make language defined packages one or the other. Probably we would want (at least in language-defined packages) to have a rule similar to the one for Postconditions: that an object that fails D_I_C is "non-conforming" (1.1.3(17.1/5) & 11.4.2(23.2-3/5)). For other types, it certainly would be OK for P_I and D_I_C to be compatible if A_P is Ignore -- presuming the problem is meeting C.4(11) [that there is no language-defined check that can fail] rather than the idea of having a contract. (Couldn't resist with the acronyms.) Even so, that's not really necessary, as C.4(11) is really only defining the cases that must not generate code, and a contract is a "check" (so a check that might fail can generate code). C.4(14) only suggests "little or no code"; there's no requirement (and no advice, either) that there be *no* code. So I don't think there is any need to prevent D_I_C and P_I from being used together; if there is a problem for user-defined code, pragma Assertion_Policy (Ignore, Default_Initial_Condition); will eliminate the generated code. **************************************************************** From: Tucker Taft Sent: Monday, March 19, 2018 10:25 PM > ... > So I don't think there is any need to prevent D_I_C and P_I from being > used together; if there is a problem for user-defined code, pragma > Assertion_Policy (Ignore, Default_Initial_Condition); will eliminate > the generated code. I think I agree. We don't want to rule out the combination of D_I_C and P_I. The run-time check associated with D_I_C, in the case of a preelaborable construct, must necessarily involve data that is knowable prior to run-time, so, if the implementation cannot evaluate it at compile/link time, it could be deferred to the point of the first executable code. **************************************************************** From: Steve Baird Sent: Wednesday, March 28, 2018 6:56 PM As per Randy's suggestion, here is preliminary wording [this is version /01 of the AI - ED] for a proposed Default_Initial_Condition aspect (with no mention here of the Initial_Condition aspect for packages). > For example, > > package Sets is > type Set is private > with Default_Initial_Condition => Is_Empty (Set); > function Is_Empty (S : Set) return Boolean; > ... > end; **************************************************************** From: Randy Brukardt Sent: Wednesday, March 28, 2018 11:22 PM > As per Randy's suggestion, here is preliminary wording for a proposed > Default_Initial_Condition aspect (with no mention here of the > Initial_Condition aspect for packages). Thanks for doing this, it saved me some work. OTOH, the missing !problem and !discussion might be issues someday. > ==== > > 7.6.2 Default Initial Conditions > > For a private type or private extension, the following > language-defined aspect may be specified with an aspect_specification > (see 13.1.1): > > Default_Initial_Condition > > This aspect shall be specified by an expression, called a default > initial condition expression. > Default_Initial_Condition may be specified on a > private_type_declaration or a private_extension_declaration. > > [TBD: do we want to allow it on a completion, as is done with type > invariants? It seems that hiding it in the private part would defeat > the purpose of this aspect.] I doubt it, I agree that hiding it makes no sense, just like hiding preconditions makes no sense. OTOH, we probably need a class-wide version and inheritance thereof. It seems that if one is depending on class-wide properties, an extension that didn't meet such a property could be a problem. (It's hard to imagine why we would need class-wide type invariants and not a class-wide version of this aspect. > Legality Rules > > The Default_Initial_Condition aspect shall not be specified for > a type whose partial view has unknown > discriminants [, whether explicitly declared or inherited]. > > [TBD: is this the right wording? The intent here is to disallow the > case where a client who sees only the partial view could never declare > a default-initialized object of the type. The wording seems OK, and the reason seems legitimate. Not sure if it applies to a class-wide version. > ... Note that it would be wrong to disallow a D_I_C for an abstract > type because a client might extend the type and then declare a > default-initialized object of the extension type.] The latter only makes sense for the class-wide (inherited by extensions) version. The specific aspects are never inherited, so abstract versions don't make sense. > Static Semantics > > [If the Default_Initial_Value aspect is specified for a type T, then > the default initial condition expression applies to T and to all > descendants of T.] This is the property of a class-wide contract. Specific contracts aren't inherited. It seems your rules are just a bit confused over which it wants to be. ... > In 11.4.2, find everywhere that type invariants are mentioned and > update to also mention default initial conditions: > > Assert pragmas, subtype predicates (see 3.2.4), preconditions and > postconditions (see 6.1.1), > {default initial conditions (see 7.6.2),} > and type invariants (see 7.3.2) are collectively referred > to as assertions; > > Any postcondition expression > {, default initial condition expression,} > or type invariant expression occurring in the specification of a > language-defined unit is enabled (see 6.1.1 {, 7.3.2,} and 7.3.2). We also need to make a similar update to 1.1.3(17.1/5): For an implementation that conforms to this Standard, the implementation of a language-defined unit shall abide by all postconditions{, default initial conditions,} and type invariants specified for the unit by this International Standard (see 11.4.2). **************************************************************** From: Randy Brukardt Sent: Wednesday, March 28, 2018 11:40 PM I added the following discussion to the AI, since Steve didn't provide one: --- Editor's take [since the author didn't provide one]: If one imagines that the default initialization of the object is described by a function D_I, this contract describes the postcondition of that (imaginary) function. In this postcondition, the current instance of the type takes the place of D_I'Result, and the only parameters could be the bounds or discriminants of the type (so 'Old is not useful). Therefore, we don't need any of those special capabilities in Default_Initial_Condition as would do in real postconditions. The comparison to postconditions answers various other questions: the contract shouldn't be hidden, we ought to have both specific and class-wide versions, only the class-wide version is inherited, etc. --- I think this "equivalence" provides a relatively simple model of the new contract to answer any questions that come up as to how it should work, although we might be able to justify simplifying it further. **************************************************************** Editorial Review from Randy Brukardt [private mail] I see the AI gives the proposed subclause for this new contract as 7.6.2; that seems weird. 7.6 and 7.6.1 are about finalization and completion, and this AI is about initialization. It doesn't seem to belong there. The subclause clearly goes in Chapter (er, Clause) 7, but I think it makes more sense directly after type invariants. (That's a bit of an issue, as Stable Properties has already been added there, but that's a relatively easy change.) Both the type invariant and stable properties are about contracts on private types, and this is also a contract on a private type. Tucker Taft: I agree with your reasoning. It is a contract on private types, and probably deserves to be near Type Invariants. ****************************************************************