CVS difference for 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