CVS difference for ai12s/ai12-0405-1.txt
--- ai12s/ai12-0405-1.txt 2020/12/04 07:59:30 1.3
+++ ai12s/ai12-0405-1.txt 2020/12/11 22:22:26 1.4
@@ -1,6 +1,8 @@
-!standard 7.3.4(10/5) 20-12-02 AI12-0405-1/01
+!standard 7.3.4(10/5) 20-12-11 AI12-0405-1/02
!standard 7.3.4(15/5)
!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
@@ -27,7 +29,7 @@
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.)
+ 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
@@ -54,7 +56,7 @@
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.)
+ 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
@@ -106,38 +108,36 @@
!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.]
+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). [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.]
+ 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.
@@ -146,15 +146,15 @@
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.
+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) 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.
+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 "Global => null" function and a second rule
@@ -164,54 +164,23 @@
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.
+ worth the bother.
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.]
+Proposal A:
-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):
+ No change.
- 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):
@@ -239,45 +208,9 @@
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.
+Proposal F:
+ No change.
- 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"
@@ -335,6 +268,7 @@
!discussion
+Discussion is included in the !proposal.
!ASIS
@@ -832,23 +766,4 @@
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