Version 1.5 of ai12s/ai12-0195-1.txt

Unformatted version of ai12s/ai12-0195-1.txt version 1.5
Other versions for file 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