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

Differences between 1.3 and version 1.4
Log of other versions for file ai12s/ai12-0405-1.txt

--- ai12s/ai12-0405-1.txt	2020/12/04 07:59:30	1.3
+++ ai12s/ai12-0405-1.txt	2020/12/11 22:22:26	1.4
@@ -1,6 +1,8 @@
-!standard 7.3.4(10/5)                                  20-12-02  AI12-0405-1/01
+!standard 7.3.4(10/5)                                  20-12-11  AI12-0405-1/02
 !standard 7.3.4(15/5)
 !class Amendment 20-10-21
+!status Amendment 1-2012 20-12-11
+!status ARG Approved 15-0-0  20-12-09
 !status work item 20-10-21
 !status received 20-10-21
 !priority Low
@@ -27,7 +29,7 @@
 
 B) With the current rules, stable property checks are never performed
    for an access parameter (that is, a parameter of an anonymous access type).
-   Is this a problem that should be fixed? (Yes.)
+   Is this a problem that should be fixed? (No.)
 
 C) With the current RM wording, it is unclear what equality operator
    is used for "F(P) = F(P)'Old" stable property checks. Should this
@@ -54,7 +56,7 @@
    explicit specific postcondition expression prevents generation of an
      F(P) = F(P)'Old
    stable property check. Similarly in the class-wide case.
-   Is this really what was wanted? (TBD.)
+   Is this really what was wanted? (Yes.)
 
 G) The terms "stable property function" and "class-wide stable property
    function" are unnecessarily confusing (it is similar to the situation
@@ -106,38 +108,36 @@
 
 !proposal
 
-A) Two alternative subproposals, depending on how we want to go
-   with respect to the decision described in the next paragraph.
-   Either way, we disallow stable-properties checks for out-mode parameters.
-
-   This issue is about not generating certain stable property checks.
-   Two approaches have been considered. The simplest (and more permissive)
-   option is to just modify the existing rules so that the unwanted checks
-   are not generated. Another approach is based on the "that does not occur
-   in the explicit specific postcondition expression of S" clause of
-   7.3.4(21/5) and the next paragraph's analogous rule for the
-   class-wide case. The idea is that the user is required to prevent the
-   unwanted checks by means of the explicit (specific or class-wide, as the
-   case may be) postconditions; if the user fails to do this, then the
-   program is illegal.
-
-B) For a null-excluding access parameter P with a designated type T,
-   generate stable property checks for P.all as would be generated
-   for a parameter of type T. The idea here is to treat such an "access T"
-   parameter similarly to an in-out parameter of type T, as opposed
-   to like a parameter of a named access type.
-   No stable property checks for a possibly-null access parameter.
-   [If it seems preferable to avoid treating null-excluding access parameters
-   differently than those that allow null, then that's also a feasible
-   option; a null access check would have to be performed.]
+A) We modify the existing rules so that the unwanted checks
+   are not generated.
 
+B) We did not add stable property checks to anonymous access parameters.
+   It seems necessary to exclude named access types from such checks.
+   For many purposes, named access types and anonymous access types
+   work the same. And for other purposes, anonymous access types work
+   like another mode. It seems that either answer would be wrong at
+   least part of the time. Therefore, it is better to do nothing implicit;
+   a user can always explicit add any needed postconditions.
+
+   Note that if we did allow this, we would have to have an additional
+   implicit null test before the implicit postcondition; we certainly don't
+   want implicit postconditions raising Constraint_Error from dereferencing 
+   null.
+
 C) Use the same equality op that is used for "X in Y" membership tests,
-   as described in 4.5.2(28.1/5). [Randy argues that it would be
-   better to get the same results as if the user wrote an explicit
-   "F(P) = F(P)'Old" postcondition. Steve argues that we want uniformity
-   in the language definition regarding constructs which make implicit
-   use of equality; don't do it one way for membership tests and a different
-   way for this case.]
+   as described in 4.5.2(28.1/5).
+
+   We choose this because we want uniformity in the language definition 
+   regarding constructs which make implicit use of equality; we don't want to
+   do it one way for membership tests and a different way for this case.
+   And getting visibility involved with implicit constructs is uncomfortable.
+
+   The counterargument is that this will be mixed with similar postconditions
+   written explicitly, and those of course will use the visible "=". For
+   cases where an elementary or array type has a user-defined "=", explicit
+   and implicit postconditions will use different operators. We accept this
+   difference as such types are rare, and using them as the result type of
+   a stable property function will be rarer still.
 
 D) Add non-normative text clarifying the point that inherited
    subprograms may be subject to stable property checks.
@@ -146,15 +146,15 @@
    that is in effect when the subprogram is declared, even if the
    subprogram lacks an explicit Post/Post'Class aspect specification.
 
-F) Two alternative subproposals, depending on the answer to question
-   posed in the !question section.
+F) The existing wording was not the result of an oversight - it correctly 
+   captures the idea that a stable property check is omitted only if the 
+   explicit postcondition says something else about some property function
+   or if it is explicitly omitted with a *not* stable property.
 
 G) Clean things up as described in the !question section.
 
-H) For these, unlike A) above, we do not provide two subproposals.
-   We assume that we do not want to take the "explicit postcondition"
-   approach and we instead simply change the rules so that the
-   unwanted Post/Post'Class augmentation does not occur.
+H) We change the rules so that the unwanted Post/Post'Class augmentation 
+   does not occur.
 
    As part of this, we add a rule that stable property checks are
    omitted for any "Global => null" function and a second rule
@@ -164,54 +164,23 @@
    class-wide stable property functions for an abstract subprogram.
    Specific stable property functions for an abstract subprogram
    are useless, but harmless. Disallowing them doesn't seem to be
-   worth the bother, but this is obviously debatable.
+   worth the bother.
 
 I) Disallow the renaming.
 
 !wording
 
-[Subproposals are used here to present alternative solutions to a
-given problem; for example, it is intended that exactly one of
-Subproposal A.1 and subproposal A.2 will be selected. Except when
-noted otherwise, the choice of one subproposal instead of another
-should have no effect on the other parts of this AI.]
+Proposal A:
 
-Subproposal A.1:
-
    In 7.3.4(22/5) and 7.3.4(23/5) , replace
      "and P is each parameter of S that has type T" 
    with
      "and P is each parameter of S that has type T and is not of mode *out*" 
 
-Subproposal A.2:
-
-   Append a second Legality Rules section after the existing Static
-   Semantics section (there is already a preceding Legality Rules section).
-
-   Applying the postcondition modification rules described above, no
-   postcondition expression of the form P(F)=P(F)'Old shall be added
-   for a formal parameter P of mode *out*. [In other words, it is the
-   responsibility of the user to prevent such an addition by specifying
-   a (specific or class-wide) postcondition as needed.]
-
 Proposal B:
 
-Add as a new penultimate sentence in 7.3.4(22/5):
+  No change.
 
-   Similarly, a null-excluding access parameter Q whose designated type
-   is T is treated like a parameter of type T
-   [with respect to these additions to the specific postcondition
-   expression of S], except that the equality expression is of the form
-   F(P.all) = F(P.all)'Old.
-
-Add as a new penultimate sentence in 7.3.4(23/5):
-
-   Similarly, a null-excluding access parameter Q whose designated type
-   is T is treated like a parameter of type T
-   [with respect to these additions to the class-wide postcondition
-   expression of S], except that the equality expression is of the form
-   F(P.all) = F(P.all)'Old.
-
 Proposal C:
 
   Append after 7.3.4(23/5):
@@ -239,45 +208,9 @@
      Pre'Class) assertion policy that is in effect at the point of declaration
      of the subprogram S.
 
-Subproposal F.1:
-   Do nothing. Stick with the status quo. [Randy strongly favors this
-   alternative, and makes the point that the existing wording was
-   not the result of an oversight - it correctly captures the idea that
-   a stable property check is omitted only if the explicit postcondition
-   says something else about the property function in question.]
-
-Subproposal F.2:
-   In 7.3.4(22/5), replace
-      ... with one such equality included for each stable property function
-      F of S for type T that does not occur in the explicit specific
-      postcondition expression of S, and P is each parameter of S that
-      has type T.
+Proposal F:
+   No change.
 
-   with
-      ... with one such equality included for each stable property function
-      F of S for type T, and P is each parameter of S that
-      has type T and does not occur in the explicit specific
-      postcondition expression of S.
-
-   In 7.3.4(23/5), replace
-      ... with one such equality included for each class-wide stable property
-      function F of S for type T that does not occur in any class-wide
-      postcondition expression that applies to S, and P is each parameter of
-      S that has type T. 
-
-   with
-      ... with one such equality included for each class-wide stable property
-      function F of S for type T, and P is each parameter of
-      S that has type T and does not occur in any class-wide  
-      postcondition expression that applies to S. 
-
-      AARM note: If T is derived from another type TT which has a primitive
-      subprogram that mentions a formal parameter PP in its class-wide
-      postcondition expression, then the corresponding formal parameter of
-      of any corresponding inherited subprogram, or of any subprogram that
-      overrides such an inherited subprogram, occurs in a class-wide
-      postcondition that applies to S.
-
 Proposal G:
 
    7.3.4(5/5) - add the word "specific"
@@ -335,6 +268,7 @@
       
 !discussion
 
+Discussion is included in the !proposal.
 
 !ASIS
 
@@ -832,23 +766,4 @@
 Could we get the best of both options with an AARM note observing that the 
 specified "F(X) = F(X)'Old" is really equivalent to "F(X) in F(X)'Old" ?
 
-****************************************************************
-
-From: Steve Baird
-Sent: Thursday, October 22, 2020  7:38 PM
-
-****************************************************************
-
-From: Steve Baird
-Sent: Thursday, October 22, 2020  7:38 PM
-
-****************************************************************
-
-From: Steve Baird
-Sent: Thursday, October 22, 2020  7:38 PM
-
-****************************************************************
-
-From: Steve Baird
-Sent: Thursday, October 22, 2020  7:38 PM
 ****************************************************************

Questions? Ask the ACAA Technical Agent