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

Unformatted version of ai12s/ai12-0195-1.txt version 1.2
Other versions for file ai12s/ai12-0195-1.txt

!standard 6.1.1(38/4)          16-07-21 AI12-0195-1/02
!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.

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

Questions? Ask the ACAA Technical Agent