Version 1.5 of ai12s/ai12-0195-1.txt
!standard 6.1.1(38/4) 16-10-02 AI12-0195-1/03
!class binding interpretation 16-06-07
!status Amendment 1-2012 16-07-21
!status ARG Approved 6-0-5 16-06-11
!status work item 16-06-07
!status received 16-06-04
!priority Medium
!difficulty Hard
!qualifier Omission
!subject Inheriting body but overriding precondition or postcondition
!summary
If a primitive with a class-wide precondition or postcondition is inherited,
while some primitive called in the class-wide precondition or postcondition
is overridden, then a wrapper is required to check both the interpretation
for the inherited subprogram and the interpretation for the original,
non-inherited subprogram.
!question
Consider an overriding:
package Pkg7 is
type AT1 is tagged null record;
function F1 (X : AT1) return Boolean;
function F2 (Y : AT1) return Boolean
with Pre'Class => F1 (Y);
end Pkg7;
with Pkg7;
package Pkg8 is
type NT is new Pkg7.AT1;
overridding
function F1 (X : NT) return Boolean;
end Pkg8;
Consider a dispatching call:
F2 (AT1'Class(Obj_of_NT));
The precondition that the caller sees is going to call F1 (for NT).
The inherited body, OTOH, expects that the original F1 (for AT1) will be called.
Which "F1"(s) will be called? (Both.)
!recommendation
(See Summary.)
!wording
Add after 6.1.1(38/4):
For the purposes of the above rules, a call on an inherited
subprogram is considered to involve a call on a subprogram S' whose
body consists only of a call (with appropriate conversions) on the
non-inherited subprogram S from which the inherited subprogram was
derived. It is not specified whether class-wide precondition or
postcondition expressions that are equivalent (with respect to which
non-inherited function bodies are executed) for S and S' are
evaluated once or twice. If evaluated only once, the value returned
is used for both associated checks.
AARM Implementation note: If the class-wide pre- and postcondition
expressions are equivalent for S and S' because none of the
primitive subprograms called in those expressions were overridden, no
wrapper is needed. Otherwise, a wrapper is presumably needed to
provide the correct logic.
!discussion
The caller might want to be able to check in advance whether a
dispatching call is going to fail a precondition check, so they want the
precondition determined by the controlling tag to give the correct
answer. The callee wants to know that the precondition determined at
the point where the body was compiled can be presumed true. These two
conflict. To be meaningful, if a subprogram is inherited but its
class-wide precondition is changed by overriding a routine called in the
precondition expression, the new interpretation should return True only
if the original interpretation would have returned True. In other
words, the new interpretation implies the old interpretation. By
checking both, we can catch the bug where this implication is not true.
Similarly, a caller making a dispatching call wants to know that the
postcondition expression determined by the controlling tag will hold
true upon return. But the callee only knows about the postcondition
relevant at the point where the body was defined. Again, these two
conflict unless the original postcondition implies the overriding
interpretation. By checking both again we can detect the bug.
Normally we would not expect an operation to be inherited while some
part of its pre- or postcondition expression is overridden. If no such
overriding takes place, then no wrapper is necessary. But if any pre-
or postcondition expression is effectively overridden, then a wrapper is
necessary to ensure that both interpretations of the pre/postcondition
expression evaluate to True.
Another option would to evaluate every intervening interpretation, but
that seems unduly painful and inefficient, and doesn't really serve
either the caller or the callee in any useful way.
!corrigendum 6.1.1(38/4)
Insert after the paragraph:
The class-wide precondition check for a call to a subprogram or entry S
consists solely of checking the class-wide precondition expressions that apply
to the denoted callable entity (not necessarily to the one that is invoked).
Any operations within such an expression that were resolved as primitive
operations of the (notional) formal derived type NT are in the evaluation
of the precondition bound to the corresponding operations of the type
identified by the controlling tag of the call on S. This applies to both
dispatching and non-dispatching calls on S.
the new paragraph:
For the purposes of the above rules, a call on an inherited
subprogram is considered to involve a call on a subprogram S' whose
body consists only of a call (with appropriate conversions) on the
non-inherited subprogram S from which the inherited subprogram was
derived. It is not specified whether class-wide precondition or
postcondition expressions that are equivalent (with respect to which
non-inherited function bodies are executed) for S and S' are
evaluated once or twice. If evaluated only once, the value returned
is used for both associated checks.
!ASIS
This is just runtime behavior, so there should be no ASIS effect.
!ACATS Test
An ACATS C-Test should be created to ensure the extra check is made.
!appendix
From: Tucker Taft
Sent: Saturday, June 4, 2016 5:23 PM
It is possible to change the meaning of a class-wide pre/postcondition by
overriding one of the primitives called in the expression, while still
inheriting the associated subprogram. This creates a somewhat bizarre
situation, where a caller making a dispatching call and the ultimately
invoked subprogram body have different interpretations for what
pre/postconditions are checked. This AI proposes that we check both
interpretations, if they differ. This is a spin-off from AI12-0170, and
was part of the homework for that AI. [This is version /01 of this AI - Ed.]
****************************************************************
From: Randy Brukardt
Sent: Thursday, July 21, 2016 5:48 PM
For the record: When I was editing AI12-0195-1, I noticed that the AARM Note
has less-than-optimal wording. I made several (what I hope are) improvements;
this note is just to document those changes.
I changed the AARM note as marked:
AARM Implementation note: If the class-wide [pre/postcondition]
{pre- and postcondition} expressions are equivalent for S and S' because
none of the [other] primitive subprograms called in {those}[the]
expressions were overridden, no wrapper is needed. Otherwise, a wrapper
is presumably needed to provide the correct logic.
Reasons:
(1) The usual text in 6.1.1 uses "pre-" when talking about both preconditions
and postconditions. And in this case, the "and" is important; one needs a
wrapper unless all applicable class-wide precondition and postcondition
expressions have no primitive subprograms that are overridden.
(2) I deleted "other" because no other primitive routines are discussed in
this note. So other than which primitive subprograms? Moreover, even if it
is trying to exclude the routine itself for a bizarre recursive pre- or
postcondition, I think that would be wrong. So the "other" serves no
purpose other than to confuse.
(3) I thought "those" read better than "the" for this note. It ties the
expressions more strongly to the ones talked about earlier in the
sentence. Simple as that.
(4) [Not shown above]. For some reason, this text was in the AI in square
brackets, which normally would indicate a deletion (but this is an
addition). And "Redundant" brackets never apply to AARM notes (by
definition, they're all redundant to the normative wording). So I don't
know what they were doing there; I deleted them.
****************************************************************
From: Tucker Taft
Sent: Friday, July 22, 2016 4:41 PM
All your changes make sense to me!
****************************************************************
From: Brad Moore
Sent: Friday, September 9, 2016 6:58 PM
I was just doing an editorial review of the subject AI, and thought of a
possible problem that is not mentioned in the AI.
The AI suggests that a class wide precondition that calls a primitive that
is overridden, would potentially check that the overridden primitive holds
true, as well as the original primitive that was inherited.
I am wondering about such a case where both the overridden function and the
override have side effects that are not idempotent. For example, both might
increment a component of the base type. Evaluating both calls might lead to
unexpected results.
Since this isn't mentioned in the AI, I wonder if it was considered, and then
also, is the extra check still considered enough of a benefit to still be
considered to be worthwhile if it introduces this potential downside?
****************************************************************
From: Tucker Taft
Sent: Saturday, September 10, 2016 4:54 PM
> I am wondering about such a case where both the overridden function
> and the override have side effects that are not idempotent. For
> example, both might increment a component of the base type. Evaluating
> both calls might lead to unexpected results.
In general, preconditions are not expected to have side effects, and I would
say that the possibility of side effects should not be a factor in deciding
what is their desired semantics. See RM 11.4.2(26/3, 27/3) for indications
that the implementation can ignore possible side effects, and even reject
assertions that have them.
> Since this isn't mentioned in the AI, I wonder if it was considered,
> and then also, is the extra check still considered enough of a benefit
> to still be considered to be worthwhile if it introduces this potential
> downside?
I don't think issues relating to possible side effects should be relevant,
since such side effects are not recommended and run against the primary purpose
of preconditions.
****************************************************************
From: Jeff Cousins
Sent: Monday, September 12, 2016 8:25 AM
> In general, preconditions are not expected to have side effects, and I would
> say that the possibility of side effects should not be a factor in deciding
> what is their desired semantics.
> I don't think issues relating to possible side effects should be relevant,
> since such side effects are not recommended and run against the primary
> purpose of preconditions.
I go along with Tuck, it would be bad practice for functions used in
preconditions (or postconditions or type invariants, for that matter) to have
side effects, and this problem shouldn't influence this AI.
Though having said that, my ACATS tests are dependent on them having
side-effects for marking which particular functions have been called.
> See RM 11.4.2(26/3, 27/3) for indications that the implementation can ignore
> possible side effects, and even reject assertions that have them.
Maybe this is important enough that it should be controllable by the user, say
by a configuration pragma, rather than implementation defined. It's bad enough
that whether assertion checking defaults to Check or Ignore is implementation
defined.
****************************************************************
From: Randy Brukardt
Sent: Friday, September 9, 2016 9:15 PM
Generally, side effects are considered evil in contracts. Some can be rejected
by an implementation permission (see 11.4.2 I think no RM handy here on the
shore of Yellowstone Lake.) Benign side effects don't have any guarantee, much
like calls to Finalize. So I think we don't care.
****************************************************************
Questions? Ask the ACAA Technical Agent