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

--- ai12s/ai12-0405-1.txt	2020/12/17 04:15:24	1.5
+++ ai12s/ai12-0405-1.txt	2020/12/19 08:31:08	1.6
@@ -1,4 +1,4 @@
-!standard 6.1.2(19/5)                                  20-12-15  AI12-0405-1/03
+!standard 6.1.2(19/5)                                  20-12-18  AI12-0405-1/04
 !standard 7.3.4(0)
 !class Amendment 20-10-21
 !status Amendment 1-2012 20-12-11
@@ -78,10 +78,11 @@
    "+" operator for a user-defined integer type), static functions
    (if a function has an implicit postcondition, then how can a call to that
    function be a static expression?), null procedures (which are not
-   allowed to have explicit postconditions, at least in part because of the
-   8.3 "one is chosen arbitrarily" rule), and abstract subprograms
-   (which can have Post'Class specified but not Post). Should stable
-   property checks not be generated in these situations? (Yes.)
+   allowed to have explicit specific postconditions, at least in part 
+   because of the 8.3 "one is chosen arbitrarily" rule), and abstract
+   subprograms (which like null procedures can have Post'Class specified
+   but not Post). Should stable property checks not be generated in these
+   situations? (Yes.)
    
 I) In some unusual situations, the current rules imply that a renaming
    of a subprogram might get a stable-properties-related postcondition
@@ -157,15 +158,10 @@
    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
-   that all static functions are implicitly "Global => null" functions.
+   omitted for any in parameters of a "Global => null" subprogram
+   and a second rule that all static functions are implicitly
+   "Global => null" functions.
 
-   Abstract subprograms are ignored here. We want to allow
-   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.
-
 I) Disallow the renaming.
 
 !wording
@@ -177,6 +173,8 @@
    with
      "and P is each parameter of S that has type T and is not of mode *out*" 
 
+   [But we fold this into Proposal H instead.]
+
 Proposal B:
 
   No change.
@@ -237,13 +235,45 @@
       For a predefined operator of an elementary type, [or] the function
       representing an enumeration literal{, or any other static function
       (see 4.9)}, the Global aspect is null.
+
 
-   Add "otherwise, " at the start of each of the three bulleted list items
-   7.3.4(17/5, 18/5, and 19/5) and add a new first element of that
-   bulleted list
+   Add before 7.3.4(22/5):
 
-      if S is a null procedure, or if the Global aspect of S is null,
-      or if S is a stable property function of T, then no functions;
+   For a primitive subprogram S of a type T that has a parameter P of type T, 
+   the parameter is /excluded from stable property checks/ if:
+    * S is a stable property function of T;
+       AARM Reason: This prevents possible infinite recursion,
+       where the postcondition calls the function itself (directly or
+      indirectly)..
+    * P has mode *out*;
+       AARM Reason: A parameter of mode *out* doesn't necessarily have a defined
+       input value. Ideally, the postcondition will include expressions
+       defining the values of the stable properties after the call, but we
+       do not try to ensure this.
+    * the Global aspect of S is *null*, and P has mode *in* and the mode is not 
+      overridden by a global aspect.
+       AARM Reason: An *in* parameter of a Global => *null* subprogram cannot
+       be modified, even if it has indirect parts, without violating the Global
+       aspect. Thus, there is no need to assert that the properties don't
+       change.
+
+   Modify 7.3.4(22/5):
+
+     For every primitive subprogram S of a type T {that is not an abstract 
+     subprogram or null procedure}, ...
+
+   Add after 7.3.4(22/5):
+     AARM Reason: Null procedures and abstract subprograms are excluded as they
+     do not allow specific postconditions. Moreover, for null procedures, static
+     analysis tools can be certain that their parameters aren't modified so 
+     there is no need to assert that the properties don't change. Abstract
+     subprograms cannot be directly called.
+
+   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 excluded from
+      stable property checks" 
 
    Delete "that is not a stable property function" from 7.3.4(22/5)
    and 7.3.4(23/5).
@@ -794,5 +824,30 @@
 as this follows the style of similar rules and avoids any confusion about
 what is "respective". (It also sidesteps the question of whether "respectively"
 should be followed with a comma or not -- it has to be one or the other, not both.
+
+****************************************************************
+
+Editor's note, December 18, 2020
+
+After consulting with Steve Baird and Tucker Taft, I replaced the wording of
+Proposal H, folding in Proposal A.
+
+This was done mainly because simply excluding checks for subprograms with
+the Global aspect set to null is far too broad. The goal was to exclude
+stable property checks in cases (such as predefined operators and static
+functions) where it is clear that the parameter cannot be modified. Of course,
+a parameter with a mode other than *in* can be modified (that's the point!),
+and thus should have stable properties checks when appropriate. Additionally,
+the global aspect can override the mode of a parameter to reflect internal
+modifications (as in the Text_IO File parameter case), and that also needs
+to be reflected in the rules.
+
+It seemed best to fold the exclusions together, other than moving the
+null procedure/abstract subprogram case solely to the specific case (these
+do not allow Post, but they do allow Post'Class; we don't want to add
+a Post that otherwise cannot exist, but the class-wide case should work
+as usual).
+
+Some editorial changes were also made to match this wording.
 
 ****************************************************************