!standard 7.6.2(0)                                  18-03-28  AI12-0265-1/01
!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 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

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.]

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].

[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. 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.]

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.]

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.

----

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).

    The evaluation of any such postcondition {, default initial
    condition,} or type invariant expression shall

    AARM: (subtype predicates, type invariants,
          {default initial conditions, }
          preconditions and postconditions)

    Added wording that postconditions {, default initial conditions,}
    and type invariants given on language-defined units cannot fail.

!discussion

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.

!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.

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