!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
!status received 20-10-21
!priority Low
!difficulty Easy
!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.]

!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.]

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.

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

No ASIS changes needed.


!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
****************************************************************