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

Differences between 1.8 and version 1.9
Log of other versions for file ai12s/ai12-0127-1.txt

--- ai12s/ai12-0127-1.txt	2016/10/05 23:50:39	1.8
+++ ai12s/ai12-0127-1.txt	2016/10/06 00:45:55	1.9
@@ -1,4 +1,4 @@
-!standard 4.3(2)                                    16-10-05    AI12-0127-1/05
+!standard 4.3(2)                                    16-10-06    AI12-0127-1/06
 !standard 4.3(4)
 !standard 4.3.3(3)
 !standard 4.3.4(0)
@@ -98,8 +98,8 @@
 4.3.4 Delta Aggregates
 
 A (record or array) delta aggregate yields a composite value resulting from
-copying another value of the same type and then subsequently assigning to
-some (but typically not all) components of the copy.
+starting with another value of the same type and then subsequently assigning
+to some (but typically not all) components of the copy.
 
 Syntax
 
@@ -114,13 +114,13 @@
 
 Name Resolution Rules
 
-The expected type for a record_delta_aggregate shall be a record type,
+The expected type for a record_delta_aggregate shall be a single record type
 or record extension.
 
 The expected type for an array_delta_aggregate shall be a single array
 type.
 
-The expected type for the *base_*expression of any delta aggregate is
+The expected type for the *base_*expression of any delta_aggregate is
 the type of the enclosing delta_aggregate.
 
 For a record_delta_aggregate, the expected type and applicable index
@@ -137,40 +137,45 @@
 array_component_association occurring within an array aggregate of the
 type of the delta aggregate.
 
-Legality rules
+Legality Rules
 
-For a record delta aggregate, the record_component_association_list shall
+For a record_delta_aggregate, the record_component_association_list shall
 not be null record, the record_component_association shall not use the box
 symbol <>, and the component_choice_list shall not use others.
 
-For a record delta aggregate, each component_selector_name of each
+For a record_delta_aggregate, each component_selector_name of each
 component_choice_list shall denote a distinct non discriminant component of
 the type of the delta aggregate.
 
 The types of components in record_component_associations follow the same
 rules as they do for record aggregates (see 4.3.1).
 
-For an array delta aggregate, the array_component_association shall not use
+For an array_delta_aggregate, the array_component_association shall not use
 the box symbol <>, and the discrete_choice shall not be others.
 
-For an array delta aggregate, the dimensionality of the type of the
+For an array_delta_aggregate, the dimensionality of the type of the
 delta aggregate shall be 1.
 
-For a delta aggregate the expression in a
-record_component_association, or a array_component_association shall
-not be of a limited type.
-
-AARM Note: The *base_*expression may be of a limited type (for example
-a record with limited components), the above rule only makes sure we
-do not assign to such a limited component.
+For a delta_aggregate the expression in a record_component_association or a
+array_component_association shall not be of a limited type.
+
+For an array_delta_aggregate, the *base_*expression shall be of a nonlimited
+type.
 
+AARM Ramification: The *base_*expression of a record_delta_aggregate may be of
+a limited type (for example a record with limited components), the above rule
+only makes sure we do not assign to a limited component. We do not allow the
+*base_*expression of an array_delta_aggregate to be of a limited type as this
+is a useless construct (you would not be able to update anything as the
+components necessarily are also limited except in pathological cases).
+
 Dynamic Semantics
 
-The evaluation of a delta aggregate begins with evaluating the expression
-of the delta aggregate and using that value to create and initialize the
-aggregate's anonymous object.
+The evaluation of a delta_aggregate begins with evaluating the
+*base*_expression of the delta_aggregate and using that value to create and
+initialize the aggregate's anonymous object.
 
-AARM Note: This follows the same rules as for initializing the object
+AARM Discussion: This follows the same rules as for initializing the object
 denoted by 'Old (see 6.1.1) except in the case where the anonymous
 object is built in place (see 7.6).
 
@@ -179,14 +184,14 @@
 In the case of an array component, the associated index expression is
 also evaluated and used in determining the target component just as in
 any array indexing operation. As with any aggregate, evaluation of a
-delta aggregate then denotes the associated anonymous object.
+delta_aggregate then denotes the associated anonymous object.
 
 AARM Ramification: As with 'Old, this means that the underlying tag (if any)
 associated with the delta aggregate is that of the expression in
 delta_aggregate and not that of the nominal type of the expression in
 delta_aggregate.
 
-AARM To Be Honest: the anonymous object associated with the evaluation of a
+AARM To Be Honest: The anonymous object associated with the evaluation of a
 delta aggregate begins its life as a variable, not a constant (Ada RM 3.3
 notwithstanding). This must be the case because the object is initialized
 and then subsequently modified. After evaluation of the delta aggregate is
@@ -195,8 +200,8 @@
 will eventually be a constant object after the function returns its result
 via "build in place".
 
-For a record delta aggregate, the order of the subsequent assignments
-is unspecified. For an array delta aggregate, the subsequent
+For a record_delta_aggregate, the order of the subsequent assignments
+is unspecified. For an array_delta_aggregate, the subsequent
 assignments (including all associated expression evaluations) are
 performed in the order in which the array_component_association_list
 is given; within a single array_component_association, in the order of
@@ -207,23 +212,22 @@
 
 Simple use in a postcondition:
 
-  Post => D = (D'Old with delta Day => 12)
-  --  see 3.8 for type Date
+  procedure Twelfth (D : in out Date) -- see 3.8 for type Date
+     with Post => D = (D'Old with delta Day => 12);
 
-  Post => V = (V'Old with delta A .. B => 42.0, V'First => 0.0);
-  --  see 3.6 for type Vector
+  procedure The_Answer (V : in out Vector; A, B : in Integer) -- see 3.6 for type Vector
+     with Post => V = (V'Old with delta A .. B => 42.0, V'First => 0.0);
 
 The base expression can be non-trivial:
 
-  N := (Min_Cell (L) with delta Value => 42);
-  --  see 6.1 for declaration of Min_Cell
+  New_Cell : Cell := Min_Cell (Link) with delta Value => 42);
+     -- see 3.10.1 for Cell and Link; 6.1 for Min_Cell
 
-  A1 := ((1, 2, 3) with delta Integer (Random * 3.0) => 14.2);
+  A1 : Vector := ((1, 2, 3) with delta Integer (Random * 3.0) => 14.2);
   --  see 3.6 for declaration of type Vector
   --  see 6.1 for declaration of Random
 
-  R := ((D with delta Day => 12) with delta Day => 42);
-  --  see 3.8 for type Date
+  Tomorrow := ((Yesterday with delta Day => 12) with delta Month => Apr); -- see 3.8
 
 The base expression may also be class-wide:
 
@@ -236,10 +240,6 @@
 
 * the *base_*expression of a record_delta_aggregate  (see 4.3.4)
 
-Ramification: Note this does not permit the *base_*expression of an
-array_delta_aggregate to be of limited type as this is a useless
-construct (you would not be able to update anything).
-
 !discussion
 
 SPARK 2014 defines an attribute Update for this purpose. Using this
@@ -262,8 +262,9 @@
 
 We decided "No".
 
-The would have to be listed first, and require any variant section to
-be completely updated.
+They would have to be listed first, and require any variant section 
+to be completely updated. (Indeed, all discriminant-dependent components
+would have to be present.)
 
 !examples
 
@@ -277,7 +278,7 @@
       with Post => (Fighters.Colour = Black and
                     Fighters = (Fighters'Old with delta Shape => Trapazoid));
 
-Also see examples in the !wording section.
+Also see the examples in the !wording section.
 
 !ASIS
 
@@ -1484,6 +1485,144 @@
     b) the text is clearer to the casual reader as it stands and
        would probably require a clarifying note after this
        "correction".
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, October 5, 2016  7:41 PM
+
+> > A (record, array) delta aggregate yields a composite value resulting 
+> > from copying another value of the same type
+> 
+> This is informal introductory text, so I'd suggest replacing "copying" 
+> with "starting with" because the type of the aggregate can be limited. 
+> We don't want to suggest that we are copying limited values.
+
+Right. I've made an updated version of the AI with the first two of Steve's
+changes and a number of typo and formatting changes. So we can waste less
+time at the meeting enumerating typos. ;-)
+
+On this topic, it might make sense to have a note somewhere that the
+*base*_expression would have to be a new limited value (following the rules
+of 7.5); you can't use this construct to modify an existing limited object (as
+an aggregate is a new object, so using an existing object would make a copy of
+that object).
+
+[I *did not* add such a note, but we should consider it.]
+
+Also on this topic, 7.5 has an AARM Note:
+
+AARM Ramification: Note this does not permit the *base_*expression of an
+array_delta_aggregate to be of limited type as this is a useless construct
+(you would not be able to update anything).
+
+It took me a while to figure this out. I believe the point is that it isn't
+possible to have declared limited array with non-limited components. [I suspect
+that this idea is incorrect in bizarre corner cases, but it probably isn't
+worth having support for this that only useful in pathological cases.]
+
+However, if we're not going to allow limited *base*_expressions for an
+array_delta_aggregate, then we need a Legality Rule to that effect in 4.3.4.
+(And the AARM note needs to reflect that as well.) That fact would just be
+buried in 7.5, a long way from 4.3.4.
+
+[I made these changes in my update.]
+
+> > The expected type for a record_delta_aggregate shall be a record 
+> > type, or record extension.
+> >
+> > The expected type for an array_delta_aggregate shall be a single 
+> > array type.
+> 
+> Why is the word "single" missing in the record case?
+> Note that the analogous rule in 4.3.1 says "shall be a single record 
+> type or record extension".
+
+Looks like a mistake to me; there's also an extra comma. I made those changes
+in my update.
+
+> > For an array_delta_aggregates, the expected type for each 
+> > discrete_choice in an array_component_association is the index type 
+> > of type of the delta aggregate.
+> 
+> Only a language lawyer would care about this one, but ...
+> 
+> A name resolution rule shouldn't depend on a legality rule.
+> So strictly speaking this should really say something like "the first 
+> index type" even though
+>     a) later on a legality rule will impose a requirement that that
+>        the array type's dimensionality is 1; and
+>     b) the text is clearer to the casual reader as it stands and
+>        would probably require a clarifying note after this
+>        "correction".
+
+I think this is too pedantic. Who cares what index type gets used for an
+illegal aggregate? We can discuss in PA.
+
+---
+
+I also changed most of the "array delta aggregate"s to the syntax form (with
+underscores). The form without underscores informally usually is taken to mean
+the same thing as the syntax form, but not always in the RM, and I'd rather
+avoid new terms if possible. And "aggregate" is almost always in the syntax
+form in the RM.
+
+---
+
+The first rule in the Dynamic Semantics
+
+The evaluation of a delta_aggregate begins with evaluating the expression of
+the delta aggregate and using that value to create and initialize the
+aggregate's anonymous object.
+
+is missing the *base*_ prefix for the expression. (We have it, why not use
+it??) I fixed this, too.
+
+---
+
+Simple use in a postcondition:
+
+  Post => D = (D'Old with delta Day => 12)
+  --  see 3.8 for type Date
+
+  Post => V = (V'Old with delta A .. B => 42.0, V'First => 0.0);
+  --  see 3.6 for type Vector
+
+We need the declarations of D, V, A, and B here. I suggest:
+
+  procedure Twelfth (D : in out Date) -- see 3.8 for type Date
+     with Post => D = (D'Old with delta Day => 12);
+
+  procedure The_Answer (V : in out Vector; A, B : in Integer) -- see 3.6 for type Vector
+     with Post => V = (V'Old with delta A .. B => 42.0, V'First => 0.0);
+
+---
+
+  N := (Min_Cell (L) with delta Value => 42);
+  --  see 6.1 for declaration of Min_Cell
+
+Same here with L and N. I suggest using Link and Cell from 3.10.1, so
+
+  New_Cell : Cell := Min_Cell (Link) with delta Value => 42);
+     -- see 3.10.1 for Cell and Link; 6.1 for Min_Cell
+
+Next example needs a declaration of A1, which I suggest making there by adding ": Vector".
+
+Finally:
+
+  R := ((D with delta Day => 12) with delta Day => 42);
+  --  see 3.8 for type Date
+
+Needs declarations for R and D. I suggest using the objects already declared
+in 3.8. Moreover, I think it would be best if this aggregate made sense (what
+the heck is the 42th of a month??) and thus used a different component:
+
+  Tomorrow := ((Yesterday with delta Day => 12) with delta Month => Apr); -- see 3.8
+
+---
+
+Thanks again for the update; I should have messed it up enough. ;-) [I'll post
+the update once I've gotten caught up processing homework.]
 
 ****************************************************************
 

Questions? Ask the ACAA Technical Agent