CVS difference for ai12s/ai12-0265-1.txt

Differences between 1.1 and version 1.2
Log of other versions for file ai12s/ai12-0265-1.txt

--- ai12s/ai12-0265-1.txt	2018/03/29 05:41:12	1.1
+++ ai12s/ai12-0265-1.txt	2018/04/05 06:06:03	1.2
@@ -1,8 +1,10 @@
-!standard 7.6.2(0)                                  18-03-28  AI12-0265-1/01
+!standard 7.3.3(0)                                  18-04-04  AI12-0265-1/02
 !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
@@ -33,7 +35,7 @@
 
 !wording
 
-7.6.2 Default Initial Conditions
+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):
@@ -45,10 +47,6 @@
      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
@@ -60,17 +58,11 @@
      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
+    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.]
+    descendants of T.
 
 Dynamic Semantics
 
@@ -96,34 +88,43 @@
 
 ----
 
+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).
+
 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)
+Modify 11.4.2(1.1/3):
 
-    Added wording that postconditions {, default initial conditions,}
-    and type invariants given on language-defined units cannot fail.
+   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
 
-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.
@@ -135,9 +136,145 @@
 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.
+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)
+
+For a private type or private extension, the following language-defined aspect
+may be specified with an @fa<aspect_specification> (see 13.1.1):
+
+@xhang<@xterm<Default_Initial_Condition>This aspect shall be specified by an
+expression, called a @i<default initial condition expression>.
+Default_Initial_Condition may be specified on a
+@fa<private_type_declaration> or a @fa<private_extension_declaration>.>
+
+@s8<@i<Name Resolution>>
+
+The expected type for a default initial condition expression is any
+boolean type.
+
+@s8<@i<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.
+
+@s8<@i<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.
+
+@s8<@i<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 @fa<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)
+
+@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<assertions>; their boolean expressions are referred to as
+@i<assertion expressions>.
+@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<assertions>; their
+boolean expressions are referred to as @i<assertion expressions>.
+
+!corrigendum 11.4.2(9/3)
+
+@drepl
+The @i<assertion_>@fa<aspect_mark> of a @fa<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 @fa<aspect_mark>. The @i<policy_>@fa<identifier>
+shall be either Check, Ignore, or some implementation-defined @fa<identifier>.
+@dby
+The @i<assertion_>@fa<aspect_mark> of a @fa<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 @fa<aspect_mark>. The @i<policy_>@fa<identifier>
+shall be either Check, Ignore, or some implementation-defined @fa<identifier>.
+
+
+!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<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 @fa<raise_expression> that appears within the assertion expression.
+
 !ASIS
 
 [Not sure. It seems like some new capabilities might be needed,
@@ -448,5 +585,25 @@
 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