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

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

!standard 6.1.1(38/4)          16-06-07 AI12-0195-1/01
!class binding interpretation 16-06-07
!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 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/postcondition expressions are equivalent for S and S' because none of the other primitive subprograms called in the 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.
!ASIS
** TBD
!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.]

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

Questions? Ask the ACAA Technical Agent