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

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

!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 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)
Insert after the paragraph:
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.
the new paragraph:
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)
Insert new clause:
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 Rules
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.
!corrigendum 11.4.2(1.1/3)
Replace the paragraph:
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 assertions; their boolean expressions are referred to as assertion expressions.
by:
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 assertions; their boolean expressions are referred to as assertion expressions.
!corrigendum 11.4.2(9/3)
Replace the paragraph:
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, or some implementation defined aspect_mark. The policy_identifier shall be either Check, Ignore, or some implementation-defined identifier.
by:
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.
!corrigendum 11.4.2(23.1/3)
Insert after the paragraph:
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.
the new paragraphs:
Implementation Requirements
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 raise_expression 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.

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

Questions? Ask the ACAA Technical Agent