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

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

--- ai12s/ai12-0405-1.txt	2020/10/22 23:20:13	1.1
+++ ai12s/ai12-0405-1.txt	2020/12/03 06:49:16	1.2
@@ -1,4 +1,4 @@
-!standard 7.3.4(10/5)                                  20-10-21  AI12-0405-1/00
+!standard 7.3.4(10/5)                                  20-12-02  AI12-0405-1/01
 !standard 7.3.4(15/5)
 !class Amendment 20-10-21
 !status work item 20-10-21
@@ -8,30 +8,847 @@
 !subject Fixups for stable properties
 !summary
 
+Interactions between out-mode parameters and the Stable_Properties aspect
+are improved. Other Stable_Properties issues are also addressed.
+
 !problem
+
+This AI addresses several issues with stable properties.
+
+A) The current rules for determining what stable-properties-related assertions
+   are performed do not depend on the mode of formal parameters. But there is
+   general agreement that we do not want to add dependencies on the
+   incoming values of out-mode parameters. The notion of "preserving" a value
+   doesn't really make sense for an out-mode parameter; if the incoming
+   value was intended to be significant, then the parameter mode should
+   have been in-out.
+
+   Should we somehow prevent the introduction of such dependencies? (Yes.)
+
+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.)
+
+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
+   be clarified? (Yes.) It is also unclear what "and" operator is used
+   when 7.3.4 talks about conditions being "anded". Does this need to
+   be clarified? (No.)
+
+D) There seems to be a contradiction between 7.3.4(23/5) (as it applies
+   in the case of an inherited subprogram) and 3.4(27/2). Can a
+   Stable_Properties aspect specification for a derived type
+   result in stable properties checks for inherited subprograms? (Yes;
+   3.4(27/2) is incorrect in this case).
+
+E) Interactions between pragma Assertion_Policy and the Stable_Properties
+   aspect seem unclear. The stable properties rules talk about implicit
+   modification of the (specific or class-wide) postcondition expression.
+   On the other hand, the 6.1.1 wording for Post/Post'Class talks about the
+   assertion policy in effect "at the point of a corresponding aspect
+   specification applicable to a given subprogram". Since there is no
+   explicit aspect specification in this case, is clarification needed
+   here? (Yes.)
+
+F) 7.3.4 clearly states that an explicit mention of F, not P, in an
+   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.)
+
+G) The terms "stable property function" and "class-wide stable property
+   function" are unnecessarily confusing (it is similar to the situation
+   where a "generic package" is not a "package"). This has resulted in
+   errors in the current RM (e.g., in the rules of "not" exclusions).
+   Should
+      - a new term, "specific stable property function", be introduced
+        to take the place of the existing "stable property function"; and
+      - the term "stable property function" be redefined to be the
+        union of "specific stable property function" and "class-wide
+	stable property function"; and
+      - the various existing rules that reference these terms be
+        revised in order to correctly express their "obvious" intent
+   ? (Yes.)
+
+H) The current RM rules require stable property checks for
+   parameters in some situations that seem undesirable. These include
+   stable property checks for predefined operators (e.g., the predefined
+   "+" 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.)
+   
+I) In some unusual situations, the current rules imply that a renaming
+   of a subprogram might get a stable-properties-related postcondition
+   that the original subprogram lacks. Consider:
+      package Pkg is
+        pragma Assertion_Policy (Check);
+        type T is private with Stable_Properties => Is_Somnambulant;
+        function Is_Somnambulant (X : T) return Boolean;
+        package Nested is
+          procedure Not_Primitive (X : in out T);
+        end Nested;
+        procedure Primitive (X : in out T) renames Nested.Not_Primitive;
+      private
+         ...
+      end Pkg;
+    Should this situation be disallowed somehow? (Yes.)
+
+[The proposed changes for many of these are "modular" changes, in the sense
+that each can be included or removed without affecting the rest of the AI.
+In general, this "modular" property only holds for changes where
+the status quo is already well-defined (regardless of the merit of
+that definition). If the status quo has definitional problems then
+some kind of change is required.]
 
-(See ARG e-mail and Meeting 62G discussion. Steve Baird will write.
 !proposal
 
-(See Summary.)
+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.]
+
+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.]
+
+D) Add non-normative text clarifying the point that inherited
+   subprograms may be subject to stable property checks.
+
+E) Clarify that what matters is the Post/Post'Class assertion policy
+   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.
+
+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.
+
+   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.
+
+   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, but this is obviously debatable.
 
-!wording
+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.]
+
+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):
+
+   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):
+
+     The equality operation that is used in the aforementioned
+     equality expressions is as described in the case of an
+     individual membership test whose membership_choice is a
+     choice_simple_expression (see section 4.5.2).
+
+Proposal D:
+   
+  Append after 7.3.4(23/5) [and after the text added for proposal C]"
+
+     Ramification:
+       In the case of a derived type T, when the preceding rules refer to
+       "every primitive subprogram S of a type T", the referenced set of
+       subprograms includes any inherited subprograms.
+    
+Proposal E:
+
+  Append after 7.3.4(23/5) [and after the text added for proposals C and D]:
+
+     The Pre (respectively Pre'Class) expression additions described
+     above are enabled or disabled depending on the Pre (respectively,
+     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.
+
+   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"
+       This aspect defines the [specific] stable property functions of the
+       associated type.
+
+   Add after 7.3.4(6/5):
+      The specific and class-wide stable properties of a type
+      together comprise the stable properties of the type.
+
+   Delete "(including a class-wide stable property function)" from 7.3.4(10/5).
+
+   7.3.4(16/5) - add the word "specific"
+      For a primitive subprogram S of a type T, the [specific] stable
+      property functions of S for type T are:
+
+   7.3.4(22/5) - add the word "specific" once, but not twice:
+      ..., with one such equality included for each [specific] stable
+     property function F of S ... 
+
+Proposal H:
+
+   Modify 6.1.2(19/5):
+      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
+
+      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;
+
+   Delete "that is not a stable property function" from 7.3.4(22/5)
+   and 7.3.4(23/5).
+
+Proposal I:
+
+   Add at the end of the Legality Rules section of 7.3.4
+
+     If a subprogram_renaming_declaration declares a primitive
+     subprogram S of a type T, then the renamed callable entity
+     shall also be a primitive subprogram of type T and the
+     two primitive subprograms shall have the same specific
+     stable property functions and the same class-wide stable
+     property functions (see below).
+
+   The "(see below)" is added because this wording precedes the
+   text where we define the two sets of stable property functions
+   for a given subprogram. However, if we choose subproposal A.2
+   (as opposed to A.1), then there will be a second "Legality Rules"
+   section. If we do that, then this new rule can go in that
+   section and the "(see below)" can be deleted.
+      
 !discussion
 
+
 !ASIS
 
-[Not sure. It seems like some new capabilities might be needed,
-but I didn't check - Editor.]
+No ASIS changes needed.
 
-!ACATS test
 
-ACATS B- and C-Tests are needed to check that the new capabilities are
-supported.
+!ACATS test
 
+ACATS B- and C-Tests are needed to check that the changes are properly 
+supported. These probably can be part of the tests for testing the feature
+generally.
 
 !appendix
 
+From: Steve Baird
+Sent: Tuesday, October 20, 2020  2:23 PM
+
+[This topic is not intended for discussion in tomorrow's meeting. The deadline 
+for that was a while ago.]
+
+For a subprogram with a parameter P, the Stable_Properties aspect can be used 
+to implicitly augment the subprogram's postcondition with assertions of the 
+form 
+    F(P) = F(P)'Old
+where F is a single-parameter function called a property function.
+
+The wording in RM 7.3.4(22/5) includes
+    ... the specific postcondition expression of S is modified to include
+    expressions of the form F(P) = F(P)'Old, all anded with each other
+    and any explicit specific postcondition expression, 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.
+
+Note that there is no mention of parameter modes in this rule; the mode of a 
+parameter doesn't enter into this at all.
+
+Do we really want stable property checks for out-mode parameters?
+
+I'd say that adding a dependence on the incoming value of an out-mode 
+parameter P is usually a bad thing. If the incoming value was supposed 
+to matter then the parameter mode should have been in-out, not out. But 
+it is particularly bad if the type of the out-mode parameter is a scalar 
+type with no Default_Value aspect. In that case, evaluation of F(P)'Old is
+guaranteed to involve reading an uninitialized value (see 6.4.1(15) and 
+then 13.9.1(9)).
+
+Explicit 'Old attribute prefixes that involve problematic uses of out-mode 
+parameters are not a big problem in practice because it is not something 
+that users are likely to do accidentally. 
+The implicitly-generated-for-a-stable-properties-check case seems worse to 
+me because it is easier to get into this case accidentally.
+
+By not excluding out-mode parameters from stable property checks, it seems 
+like we are making it easier for users to screw up. Since this feature was 
+supposed to increase reliability and maintainability, this seems like a 
+problem.
+
+Opinions?
+
+In private discussions, Tuck has also raised the possibility of eliminating 
+stable properties checks for in-mode parameters except 'when the "overriding"
+mode is in-out'.
+
+And I have some other less important questions about Stable_Properties.
+
+For example, the wording in 7.3.4(22/5) says that we skip a stable property check
+    F(P) = F(P)'Old
+if F is mentioned in the (explicit) postcondition. Is that rule right?
+Was mention of P, not F, what was really intended to trigger skipping the check?
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, October 20, 2020  2:52 PM
+
+> ...
+> 
+> For example, the wording in 7.3.4(22/5) says that we skip a stable 
+> property check
+>   F(P) = F(P)'Old
+> if F is mentioned in the (explicit) postcondition. Is that rule right?
+> Was mention of P, not F, what was really intended to trigger skipping 
+> the check?
+
+That would make more sense to me as well.
+
+****************************************************************
+
+From: Gary Dismukes
+Sent: Tuesday, October 20, 2020  4:00 PM
+
+> ...
+> 
+> By not excluding out-mode parameters from stable property checks, it 
+> seems like we are making it easier for users to screw up. Since this 
+> feature was supposed to increase reliability and maintainability, this 
+> seems like a problem.
+> 
+> Opinions?
+
+I agree with you that the checks should be excluded for out-mode parameters.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 20, 2020  8:51 PM
+
+Starting at the end...
+
+> For example, the wording in 7.3.4(22/5) says that we skip a stable 
+> property check
+>     F(P) = F(P)'Old
+> if F is mentioned in the (explicit) postcondition. Is that rule right?
+> Was mention of P, not F, what was really intended to trigger skipping 
+> the check?
+
+First, some background:
+
+The intent of the "stable properties" mechanism is to support the use case 
+where a function determines a property for an ADT and that property is 
+well-defined for all objects of the ADT type. In such a case, static analysis 
+of the ADT should be able to determine the value of the property for many 
+use-cases and presumably be able to prove preconditions to be true among other 
+useful things. And it can do so without knowing anything about the nature of 
+the property (presuming the property function is global null, which the vast 
+majority will be).
+
+For this idea to work as intended, the property needs to be defined for all 
+objects of the ADT type. That means that the property function should have a 
+defined value for every object after every operation of the type. Ergo, the 
+property function should appear in the postcondition for every operation that 
+has a parameter of the type, period. (Typically, in addition, a 
+Default_Initial_Condition would be used to define the initial value for each 
+property function.)
+
+The stable property mechanism was created to simplify postconditions in this 
+case by providing an implicit default that the property is unchanged by an 
+operation (common for containers, I/O, etc.). The implicit default is added 
+implicitly to the postcondition of a primitive operation in any case where 
+the property function is not called on the parameter. This ensures that the 
+property is defined for *every* object of the type after *every* primitive 
+operation -- either explicitly or implicitly via the stable property 
+mechanism.
+
+---
+
+So, to answer your questions with this model in mind:
+
+For the above question, the intent is that the property function F will be 
+part of *every* postcondition for *every* primitive operation of the type.
+Just mentioning the parameter in some way in a postcondition without 
+mentioning a property function does not give a value for the property (or 
+any property). I believe we used the "any property" model in order to deal 
+with cases where the properties (there are often many, the containers have 
+up to four and Text_IO, had it been annotated, would have a similar number)
+are interrelated. The motivating example was Text_IO, where the Mode property 
+is only significant when the Is_Open property is True.
+
+Ergo, I believe that the rule given above is as intended.
+
+---
+
+> Do we really want stable property checks for out-mode parameters?
+
+Yes, with an asterisk. The model of ADTs used for stable properties assumes 
+that they always have a defined value for each property. The assumption was 
+that there was a well-defined initial value (via Default_Initial_Condition) 
+and that the data type is such that those values are preserved. If those 
+things aren't true, static analysis is going to be a lot harder.
+
+Moreover, the use case given above is trying to ensure that every property is 
+defined for *every* object after *every* primitive operation. So there is no 
+case where we don't want a stable property check if the properties are
+*not* defined in the postconditions.
+
+Now, the asterisk is that for a *out* parameter, one really shouldn't be 
+depending on the incoming properties at all, so the postcondition must (in 
+the intended use case) *always* include a definition for the appropriate 
+properties in the postcondition. Ergo, any case where the stable properties 
+check would occur would have been because the user forgot to properly define
+the properties for the out parameter.
+
+So it doesn't matter a huge amount if the check is omitted, especially if 
+compilers give a warning if the properties aren't defined. But it does break 
+the intended model that the properties are *always* defined for *every* 
+parameter of the type for *every* primitive operation. So I'd prefer to leave 
+the rules alone.
+
+---
+
+> In private discussions, Tuck has also raised the possibility of eliminating 
+> stable properties checks for in-mode parameters except 'when the "overriding" 
+> mode is in-out'.
+
+The problem with this idea is that there is no requirement that "in"
+parameters be annotated with any global annotation or one with an overriding 
+mode or even that overriding modes be supported. We have done so in the Ada 
+library, but user code is unlikely to have such contracts (certainly none of 
+mine does). But it makes sense to add postconditions and stable properties to 
+existing libraries (just as we did to the containers), and tying that 
+mechanism to contracts that may not be given seems like a mistake.
+
+The problem here is that one is conditioning whether checks are made on the 
+presence of an optional annotation. That doesn't make sense by itself. I could 
+see giving an implementation permission to omit a stable property 
+postcondition for an "in" parameter if the global specification is such that 
+that it cannot be modified (but remember that indirectness is typically 
+ignored, so one can only do this when the strict global mode is in effect).
+Probably not worth it - one hopes that static analysis will remove unneeded 
+postcondition checks anyway (not just stable properties but any such results
+that can proven to be true based on the body of the operation).
+
+---
+
+Steve asked privately:
+
+> We've got:
+>       For every primitive subprogram S of a type T that is not a stable
+>       property function of T, the specific postcondition expression of S
+>       is modified to include expressions of the form F(P) = F(P)'Old,
+>
+>    and that's pretty much all that is said about what "=" op to use.
+
+That's (sort of) intentional; the intent was to use the "=" that one would 
+use in a usual postcondition. The idea is that the implicit F(P)'Old = F(P)
+would use the same "=" that would be used if one explicitly wrote this 
+expression. That seems important to me as it might be necessary to include 
+such an expression explicitly in cases where there are multiple properties 
+only some of which are different in a postcondition. That's especially true 
+if a new stable property is added during maintenance, and that property 
+appears in the explicit postcondition. (The rules eliminate all of the 
+implicit postconditions as a group, so it could be necessary to put some of 
+them back explicitly - it would be bad if they meant something else when 
+that happened.)
+
+> Do the rules need to be clarified here along the lines of what was 
+> done for membership tests?
+
+That would mean that the predefined "=" would be used for untagged types that 
+have a user-defined "=". I don't think that is what we want, as described 
+above.
+
+It probably would make sense to include an AARM note that "=" is the usual 
+one used for an equality expression resolved as the postcondition is 
+resolved, but I don't think any normative wording change is needed.
+
+****************************************************************
+
+From: Claire Dross
+Sent: Wednesday, October 21, 2020  3:56 AM
+
+> So, to answer your questions with this model in mind:
+>
+> For the above question, the intent is that the property function F 
+> will be part of *every* postcondition for *every* primitive operation of the 
+> type. Just mentioning the parameter in some way in a postcondition without 
+> mentioning a property function does not give a value for the property 
+> (or any property). I believe we used the "any property" model in order 
+> to deal with cases where the properties (there are often many, the 
+> containers have up to four and Text_IO, had it been annotated, would 
+> have a similar number) are interrelated. The motivating example was 
+> Text_IO, where the Mode property is only significant when the Is_Open 
+> property is True.
+
+Honestly, I am not convinced. What if the parameter is passed by copy?
+I think this would really be counter-intuitive to assume the preservation of 
+anything if the parameter is neither copied nor default initialized on 
+subprogram entry.
+
+> Now, the asterisk is that for a *out* parameter, one really shouldn't 
+> be depending on the incoming properties at all, so the postcondition 
+> must (in the intended use case) *always* include a definition for the 
+> appropriate properties in the postcondition. Ergo, any case where the 
+> stable properties check would occur would have been because the user 
+> forgot to properly define the properties for the out parameter.
+
+This I can buy, but then, I would rather not silently add an erroneous call 
+to the postcondition but rather warn the user that the property is not known
+to be preserved because of the parameter mode.
+
+> The problem here is that one is conditioning whether checks are made 
+> on the presence of an optional annotation.
+
+I strongly agree with that. I think it would complicate the rules for hardly 
+any gain.
+
+> ---
+>
+> Steve asked privately:
+>
+> > We've got:
+> >       For every primitive subprogram S of a type T that is not a stable
+> >       property function of T, the specific postcondition expression of S
+> >       is modified to include expressions of the form F(P) = F(P)'Old,
+> >
+> >    and that's pretty much all that is said about what "=" op to use.
+>
+> That's (sort of) intentional; the intent was to use the "=" that one 
+> would use in a usual postcondition. The idea is that the implicit 
+> F(P)'Old = F(P) would use the same "=" that would be used if one 
+> explicitly wrote this expression.
+
+This is pretty unfortunate if you are implementing a verification tool I would 
+say, because Ada regular equality might be less precisely known than part by 
+part comparison for example. But I agree it would be complicated to use 
+another operator here.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, October 21, 2020  8:37 AM
+
+...
+>> Now, the asterisk is that for a *out* parameter, one really shouldn't 
+>> be depending on the incoming properties at all, so the postcondition 
+>> must (in the intended use case) *always* include a definition for the 
+>> appropriate properties in the postcondition. Ergo, any case where the 
+>> stable properties check would occur would have been because the user 
+>> forgot to properly define the properties for the out parameter.
+> 
+> This I can buy, but then, I would rather not silently add an erroneous 
+> call to the postcondition but rather warn the user that the property 
+> is not known to be preserved because of the parameter mode.
+
+I agree with this.  Implicitly introducing any reference to the incoming 
+value of an OUT parameter seems like a mistake.  The compiler can be friendly 
+by "encouraging" the user to specify the value of a stable property on an OUT 
+parameter, or the language could require that every stable property be 
+specified for an OUT parameter, but we definitely do *not* want to implicitly 
+insert some code that claims it is preserved for an OUT parameter, as that 
+makes no sense.
+
 ****************************************************************
 
+From: Randy Brukardt
+Sent: Wednesday, October 21, 2020  6:53 PM
+
+> This is pretty unfortunate if you are implementing a verification tool 
+> I would say, because Ada regular equality might be less precisely 
+> known than part by part comparison for example. But I agree it would 
+> be complicated to use another operator here.
+
+To expand on my original answer a bit, in the intended use case, there will 
+be a number of explicit postconditions describing the value of the property 
+function, and some implicit postconditions describing that the value of the 
+property function is unchanged.
+
+Those explicit postconditions are most likely going to be of the form 
+F(P) = <some expression>, and those will necessarily use the visible "=" 
+(as does any explicit Ada expression). That "=" might be user-defined for 
+some types, and that will be the one used in postconditions (and 
+preconditions and almost everywhere else, only excluding some generics and 
+memberships).
+
+If the *implicit* postconditions always used the predefined "=", then one 
+would possibly be using different "=" for the explicit and implicit 
+postconditions. Quite possibly one could get different answers for the same 
+values. I'm sure a verification tool can keep that straight, but what about 
+the poor human reader (and worse, writer)? That looks like trouble to me.
+
+The verification tool is already using user-defined "=" in the (explicit) 
+postcondition, so doing so in the implicit parts can't be any harder. 
+(Admittedly, that complicates things, but that seems like a standard part 
+of analyzing Ada code -- you can't just assume = and := and () only do the 
+predefined things.)
+
+****************************************************************
+
+From: Steve Baird
+Sent: Thursday, October 22, 2020  7:38 PM
+
+> If the*implicit*  postconditions always used the predefined "=", then 
+> one would possibly be using different "=" for the explicit and 
+> implicit postconditions. Quite possibly one could get different 
+> answers for the same values. I'm sure a verification tool can keep 
+> that straight, but what about the poor human reader (and worse, writer)? 
+> That looks like trouble to me.
+
+I'll reformulate the argument I made at the meeting.
+
+Whenever we invent a construct that makes use of equality without having an 
+explicit name denoting the operator, I think that we ought to use the same 
+rules for defining what equality we are talking about.
+
+We don't want subtly different equality rules for different contexts.
+
+By that argument, stable property checks should use the equality rules 
+described in 4.5.2(28.1/5) for a membership test with a
+choice_simple_expression:
+    If the tested type is a record type or a record extension ... the
+    test uses the primitive equality for the type; otherwise, the test
+    uses predefined equality.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, October 22, 2020  9:51 PM
+
+If we do that, we need to literally use membership in the expression (not 
+"="), in the hopes of encouraging people to note that they can be different.
+Indeed, one would want users to use membership in their explicit 
+postconditions as well.
+
+As Tucker says, this is likely be moot in most real cases, since property 
+functions usually return Booleans or other scalar values that don't have any
+user-defined equality.
+
+I'd guess the issue would show up mainly if someone had a property that 
+returned a quadrangle [size/position] or complex value, both of which probably 
+are implemented as untagged records possibly with a user-defined equality. 
+Not sure how much to worry about this. (The Ada complex type does not have a
+user-defined equality, pretty much the only operation not defined
+explicitly.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, October 22, 2020  8:33 PM
+
+>> If the*implicit*  postconditions always used the predefined "=", then 
+>> one would possibly be using different "=" for the explicit and 
+>> implicit postconditions. Quite possibly one could get different 
+>> answers for the same values. I'm sure a verification tool can keep 
+>> that straight, but what about the poor human reader (and worse, writer)? 
+>> That looks like trouble to me.
+>
+> I'll reformulate the argument I made at the meeting.
+> 
+> Whenever we invent a construct that makes use of equality without 
+> having an explicit name denoting the operator, I think that we ought 
+> to use the same rules for defining what equality we are talking about.
+> 
+> We don't want subtly different equality rules for different contexts.
+> 
+> By that argument, stable property checks should use the equality rules 
+> described in 4.5.2(28.1/5) for a membership test with a
+> choice_simple_expression:
+>   If the tested type is a record type or a record extension ... the
+>   test uses the primitive equality for the type; otherwise, the test
+>   uses predefined equality.
+
+Hmmm...  Both you and Randy have good arguments, in my view.  Membership tests
+are generally between an unknown value and one or more known values.  Of 
+course you can pervert it a bit and invert the sense, but generally one 
+presumes <variable> in <known-value-set>.
+
+On the other hand, what we have with a stable property is:
+
+   <new-value-of-property> "equals" <old-value-of-property>
+
+That is a pretty different context.  It seems somewhat more likely that you 
+might want a user-defined equality here, because you have a user-defined 
+notion of "equivalence."
+
+But probably most property values will be of simple scalar types with 
+predefined equality.   And inside generics we know we fall back to the rule 
+you identified for equality, and a stable property feels a bit like a generic 
+notion like "Property is stable" that gets instantiated repeatedly with a 
+given value type returned by a property function operating on objects of the
+abstract type.
+
+Put that all together and I guess I fall somewhat more in favor of Steve's 
+argument, that we should use then normal rules for equality operator 
+"emergence" and composability, rather than relying on visibility (which I 
+find very bad news) or on always using the primitive equality, which would be 
+nice, but has never been used anywhere in the language before.
+
+And of course this is all moot if 98% of the property functions return simple 
+scalar values using a predefined "=" operator.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, October 23, 2020  1:50 PM
+
+>>By that argument, stable property checks should use the equality rules 
+>>described in 4.5.2(28.1/5) for a membership test with a ...
+
+> If we do that, we need to literally use membership in the expression 
+> (not "="),
+
+I thought about that possibility too; I see its appeal.
+
+The biggest drawback IMO is that it makes it somewhat harder for users to 
+understand what is going on when they are first getting acquainted with 
+this feature.
+
+The meaning seems easier to grasp for a check of the form
+      F(X) = F(X)'Old
+versus
+      F(X) in F(X)'Old
+even if the latter is really more precise (because it doesn't introduce any 
+questions about what equality op we are talking about).
+
+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