Version 1.7 of ai12s/ai12-0405-1.txt

Unformatted version of ai12s/ai12-0405-1.txt version 1.7
Other versions for file ai12s/ai12-0405-1.txt

!standard 6.1.2(19/5)          21-05-20 AI12-0405-1/05
!standard 7.3.4(0)
!class Amendment 20-10-21
!status Amendment 1-2012 20-12-11
!status ARG Approved 15-0-0 20-12-09
!status work item 20-10-21
!status received 20-10-21
!priority Low
!difficulty Medium
!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? (No.)
C) With the current RM wording, it is unclear what equality operator
is used for "F(P) = F(P)'Old" stable property checks. Should this 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? (Yes.)
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 specific postconditions, at least in part because of the 8.3 "one is chosen arbitrarily" rule), and abstract subprograms (which like null procedures can have Post'Class specified but not Post). Should stable property checks not be generated in these situations? (Yes.)
I) In some unusual situations, the current rules imply that a renaming
of a subprogram might get a stable-properties-related postcondition 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) We modify the existing rules so that the unwanted checks
are not generated.
B) We did not add stable property checks to anonymous access parameters.
It seems necessary to exclude named access types from such checks. For many purposes, named access types and anonymous access types work the same. And for other purposes, anonymous access types work like another mode. It seems that either answer would be wrong at least part of the time. Therefore, it is better to do nothing implicit; a user can always explicit add any needed postconditions.
Note that if we did allow this, we would have to have an additional implicit null test before the implicit postcondition; we certainly don't want implicit postconditions raising Constraint_Error from dereferencing null.
C) Use the same equality op that is used for "X in Y" membership tests,
as described in 4.5.2(28.1/5).
We choose this because we want uniformity in the language definition regarding constructs which make implicit use of equality; we don't want to do it one way for membership tests and a different way for this case. And getting visibility involved with implicit constructs is uncomfortable.
The counterargument is that this will be mixed with similar postconditions written explicitly, and those of course will use the visible "=". For cases where an elementary or array type has a user-defined "=", explicit and implicit postconditions will use different operators. We accept this difference as such types are rare, and using them as the result type of a stable property function will be rarer still.
D) Add non-normative text clarifying the point that inherited
subprograms may be subject to stable property checks.
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) The existing wording was not the result of an oversight - it correctly
captures the idea that a stable property check is omitted only if the explicit postcondition says something else about some property function or if it is explicitly omitted with a not stable property.
G) Clean things up as described in the !question section.
H) We change the rules so that the unwanted Post/Post'Class augmentation
does not occur.
As part of this, we add a rule that stable property checks are omitted for any in parameters of a "Global => null" subprogram and a second rule that all static functions are implicitly "Global => null" functions.
I) Disallow the renaming.
!wording
Proposal A:
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"
[But we fold this into Proposal H instead.]
Proposal B:
No change.
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 4.5.2).
Proposal D:
Append after 7.3.4(23/5) [and before the text added for proposal C]"
AARM 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 Post expression additions described above are enabled or disabled depending on the Post assertion policy that is in effect at the point of declaration of the subprogram S. A similar rule applies to the Post'Class expression additions.
Proposal F:
No change.
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 before 7.3.4(22/5):
For a primitive subprogram S of a type T that has a parameter P of type T, the parameter is /excluded from stable property checks/ if:
* S is a stable property function of T;
AARM Reason: This prevents possible infinite recursion, where the postcondition calls the function itself (directly or
indirectly)..
* P has mode *out*;
AARM Reason: A parameter of mode out doesn't necessarily have a defined input value. Ideally, the postcondition will include expressions defining the values of the stable properties after the call, but we do not try to ensure this.
* the Global aspect of S is *null*, and P has mode *in* and the mode is not overridden by a global aspect.
AARM Reason: An in parameter of a Global => null subprogram cannot be modified, even if it has indirect parts, without violating the Global aspect. Thus, there is no need to assert that the properties don't change.
Modify 7.3.4(22/5):
For every primitive subprogram S of a type T {that is not an abstract subprogram or null procedure}, ...
Add after 7.3.4(22/5):
AARM Reason: Null procedures and abstract subprograms are excluded as they do not allow specific postconditions. Moreover, for null procedures, static analysis tools can be certain that their parameters aren't modified so there is no need to assert that the properties don't change. Abstract subprograms cannot be directly called.
In 7.3.4(22/5) and 7.3.4(23/5), replace
"and P is each parameter of S that has type T"
with
"and P is each parameter of S that has type T and is not excluded from stable property checks"
Delete "that is not a stable property function" from 7.3.4(22/5) and 7.3.4(23/5).
Proposal I:
Add at the end of the Legality Rules section of 7.3.4
If a subprogram_renaming_declaration declares a primitive subprogram 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.
!discussion
Discussion is included in the !proposal.
!corrigendum 6.1.2(0)
Insert new clause:
See the conflict file for the changes.
!corrigendum 7.3.4(0)
Insert new clause:
See the conflict file for the changes.
!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" ?

****************************************************************

Editor's note, December 15, 2020

I replaced the wording of Proposal E:

     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.

with:

     The Pre expression additions described above are enabled or disabled 
     depending on the Pre assertion policy that is in effect at the point of
     declaration of the subprogram S. A similar rule applies to the 
     Pre'Class expression additions.

as this follows the style of similar rules and avoids any confusion about
what is "respective". (It also sidesteps the question of whether "respectively"
should be followed with a comma or not -- it has to be one or the other, not both.

****************************************************************

Editor's note, December 18, 2020

After consulting with Steve Baird and Tucker Taft, I replaced the wording of
Proposal H, folding in Proposal A.

This was done mainly because simply excluding checks for subprograms with
the Global aspect set to null is far too broad. The goal was to exclude
stable property checks in cases (such as predefined operators and static
functions) where it is clear that the parameter cannot be modified. Of course,
a parameter with a mode other than *in* can be modified (that's the point!),
and thus should have stable properties checks when appropriate. Additionally,
the global aspect can override the mode of a parameter to reflect internal
modifications (as in the Text_IO File parameter case), and that also needs
to be reflected in the rules.

It seemed best to fold the exclusions together, other than moving the
null procedure/abstract subprogram case solely to the specific case (these
do not allow Post, but they do allow Post'Class; we don't want to add
a Post that otherwise cannot exist, but the class-wide case should work
as usual).

Some editorial changes were also made to match this wording.

****************************************************************

From the WG 9 review, Issue #145

This speaks of "Pre expressions", but should surely speak of "Post 
expressions". Ditto Pre'Class => Post'Class.

[Reply from Tucker Taft:
Good catch. It is actually wrong in the AI as well (AI12-0405-1).]

[Editor's note: This will processed as an Editorial Review change on 
AI12-0405-1.]

****************************************************************

Questions? Ask the ACAA Technical Agent