!standard 13.3.2(19/3)                                 11-03-21  AI05-0247-1/01
!reference AI05-0145-2
!class Amendment 11-03-21
!status work item 11-03-21
!status received 11-03-17
!priority High
!difficulty Hard
!subject Preconditions, Postconditions, multiple inheritance, and dispatching calls

!summary

** TBD **

!proposal

The wording of 13.3.2(19/3) makes it clear that the preconditions and postconditions
(along with type_invariants, these are collectively called contract aspects here)
that apply to a dispatching call are those of the actual body. However, this rule
causes logical problems when contract aspects are added by multiple inheritance.

Consider:

    package Pack1 is
       type T1 is tagged private;
       function Is_Valid (Obj : T1) return Boolean;
       procedure P1 (Obj : in out T1);
       procedure P3 (Obj : in T1)
          with Pre'Class => Is_Valid (Obj);
    private
       ...
    end Pack1;

    package Pack2 is
       type I2 is interface;
       function Is_Green (Obj : I2) return Boolean is abstract;
       procedure P1 (Obj : in out I2) is null
           with Post'Class => Is_Green (Obj);
       procedure P2 (Obj : in I2) is null
           when Pre'Class => Is_Green (Obj);
       procedure P3 (Obj : in I2) is null
           when Pre'Class => Is_Green (Obj);
       function Something_Green return I2 is abstract
           when Post'Class => Is_Green (Something_Green'Result);
    end Pack2;

    with Pack1, Pack2;
    package Pack3 is
       type T3 is new Pack1.T1 and Pack2.I2 with private;
       overriding
       function Is_Green (Obj : T3) return Boolean;
       overriding
       procedure P2 (Obj : in T3);
       overriding
       function Something_Green return T3;
       -- P1 and P3 are inherited from Pack1.P1 and Pack1.P3,
       -- respectively.
    private
       ...
    end Pack3;

    with Pack1, Pack3;
    procedure Main is
        procedure Do_It (Obj : in Pack3.T3'Class) is
        begin
           Obj.P1; -- (1)
           Obj.P2; -- (2)
        end Do_It;
        O3 : P3.T3;
    begin
        Do_It (O3);
    end Main;

The dispatching call to P1 at (1) will call P1.P1, inherited from type T1. This
P1 has no postcondition, so Is_Green will not be called on exit from P1.
However, the following call to P2 at (2) will call Pack3.P2; it will inherit the
precondition from the interface. Thus Is_Green will be called on entrance to P2.
If P1 returned a value for which Is_Green is False (perhaps because the
programmer forgot to override P1 for type T3), the *precondition* on the call to
P2 would fail. But that is bizarre; given the postcondition matches the
precondition for the type of the calls, it will be totally mysterious to the
programmer as to why the failure is there.

It has been suggested that the contract aspects of an inherited routine ought to
be considered the same as those for an overriding routine declared at the same
point. (This would require nothing more than the compiler generating a wrapper
at this point.) But that brings up a new problem. Consider the following:

    with Pack1, Pack2, Pack3;
    procedure Main2 is
        procedure Do_It (Obj : in Pack2.T2'Class) is
        begin
           Obj.P3; -- (3)
        end Do_It;
    begin
        Do_It (P3.Something_Green);
    end Main2;

The effective precondition for the call at (3) (assuming that inherited routines
have the same contract aspects as an overriding routine) is Is_Green(Obj) or
Is_Valid(Obj). The call at (3) has to pass its precondition, as Is_Green(Obj)
has to be true (based on the postcondition of Something_Green, which creates the
object passed in). However, this means that we know nothing about Is_Valid(Obj):
it might in fact be False. And if it is, the (inherited) body of Pack1.P3 is
going to be mighty surprised to get an object that violates its precondition
(since of course it knows nothing about Is_Green).

[Editor's note: The rest of this is a proposed solution, which may or may not be
a good idea...]

The key to a solution is to realize that Preconditions and Postconditions are
different and require different rules for dispatching calls. As we noted above,
getting postconditions to work properly just requires ensuring that in any case
where a postcondition is added by an interface that the added postcondition is
reflected in the called routine. Any dispatching call would have to expect the
same or a weaker postcondition; thus, it is OK for postconditions to be those of
the body (modulo ensuring that the body evaluates any newly added
postconditions).

But this does not work for the preconditions of dispatching calls. The only
precondition that the writer of a dispatching call can know about is that of the
routine being called; that typically is stronger than the precondition of the
actual body being called. It makes no sense to enforce any other preconditions
at the point of the call of a dispatching routine (and, in particular to enforce
a weaker precondition that might apply to some body). Moreover, since any body
necessarily has a weaker precondition, this stronger precondition is the only
one that needs to be tested to get consistency. For instance, in the example
above, the precondition of the call at (3) is Is_Green(Obj) [as this is a
dispatching call to Pack2.P3]; this is stronger than the actual precondition of
the (implicit) body Pack3.P3. And it is completely different than the
precondition of the (inherited) actual body Pack1.P3 (which is Is_Valid(Obj)).

The precondition of the inherited routine seems wrong. But that's simply because
preconditions can't change by inheritance; they have to be rechecked for
inherited routines. The way to think about what is required is to imagine that
the inherited routine was in fact written explicitly. In the case of Pack3.P3,
the body would presumably look like:

    procedure P3 (Obj : in T3) is
    begin
        Pack1.P3 (Pack1.T1 (Obj)); -- (4)
    end P3;

The call to Pack1.P3 at (4) has a precondition of Is_Valid(Obj); this
precondition has to be evaluated at this call because the precondition of
Pack3.P3 is weaker (Is_Green(Obj) or Is_Valid(Obj)). Thus we end up checking the
precondition of the actual body in this case, not the weaker precondition of the
body Pack3.P3. Indeed, the effect is to *and* the preconditions (since we also
have to check the precondition expected by the interface dispatching call).
OTOH, a dispatching call using an object of T1'Class does not need to check
Is_Green at all.

...



!wording


!discussion

This issue originally came up because null procedures are considered the same
when inherited, so a dispatching call may call an arbitrary one. That however,
does not work if the null procedures have different preconditions,
postconditions, or type_invariants -- that case, the routines are
distinguishable. The solution here has to address this case as well as the more
general problems of inheritance.


!corrigendum 13.3.2(0)

@dinsc

Force a conflict; the real text is found in the conflict file.


!ACATS test

No additional ACATS test is needed here.

!ASIS

No impact on ASIS.

!appendix

From: Steve Baird
Sent: Thursday, March 3, 2011  3:28 PM

[This thread was split from AI05-0197-1]

Problem #2:

Making an arbitrary choice among null procedures assumes that they are
interchangeable, and leads to problems if they are not.

Consider the following example:

    declare
       package Pkg1 is
           type Ifc is interface;
           procedure Op (X : in out Ifc) is null;
       end Pkg1;

       package Pkg2 is
          type T is tagged null record
            with Type_Invariant => Is_Valid (T);
          procedure Op (X : in out T) is null;
          function Is_Valid (X : T) return Boolean;
       end Pkg2;
       package body Pkg2 is ... end Pkg2;

       package Pkg3 is
          type D is new Pkg1.T and Pkg2.Ifc with null record;
       end Pkg3;
    begin ...; end;

Does a dispatching call to Pkg3.Op where the tag of the controlling operand is
Pkg3.D'Tag result in a call to Is_Valid?

It seems like it depends on the "arbitrary" choice mentioned in this AI's new
wording for 3.9.2(20.2/2), which defines the dynamic semantics of such a
dispatching call:

   * otherwise, the action is the same as the action for the
     corresponding operation of the parent type or progenitor
     type from which the operation was inherited. {If there is
     more than one such corresponding operation, the action is
     that for the operation that is not a null procedure, if any;
     otherwise, the action is that of an arbitrary one of the
     operations.}

If we flip a coin to decide which from among two candidates is the
"corresponding operation ... from which the operation was inherited", and if
exactly one of these two candidates includes a call to Is_Valid in its dynamic
semantics, then it seems like we have a problem.

Both here and when 8.3(12.3/2) says "one is chosen arbitrarily", we are relying
on the premise that syntactically null procedures with appropriately conformant
profiles are interchangeable with respect to dynamic semantics.

One approach to this problem (which Randy can explain his views on in a separate
message) would involve two steps:

    1) In these two arbitrary-choice situations (3.9.2 and 8.3),
       we add a preference rule preferring operations inherited
       from a non-interface type over operations inherited from
       an interface type.

    2) We take whatever steps are needed (possibly none?)
       in order to ensure that null procedures which are primitive ops
       of interface types really are interchangeable (e.g., we
       already disallow pre and post conditions for null procedures).

This issue needs more work.

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

From: Randy Brukardt
Sent: Friday, March 4, 2011  1:15 AM

...
> Both here and when 8.3(12.3/2) says "one is chosen arbitrarily", we
> are relying on the premise that syntactically null procedures with
> appropriately conformant profiles are interchangeable with respect to
> dynamic semantics.
>
> One approach to this problem (which Randy can explain his views on in
> a separate message) would involve two steps:
>
>     1) In these two arbitrary-choice situations (3.9.2 and 8.3),
>        we add a preference rule preferring operations inherited
>        from a non-interface type over operations inherited from
>        an interface type.
>
>     2) We take whatever steps are needed (possibly none?)
>        in order to ensure that null procedures which are primitive ops
>        of interface types really are interchangeable (e.g., we
>        already disallow pre and post conditions for null procedures).
>
> This issue needs more work.

I don't really have any views specifically on this problem, but the discussion
of it has gotten me very concerned that there is something fundamentally wrong
with the way we handle Pre/Post/Type_Invariant aspects on dispatching calls.
I'll call these "contract aspects" in the discussion below; most of the points
apply to all three of them.

Tucker has explained that the contract aspects that apply to a particular
subprogram body are always determined when that subprogram is declared. In
particular, inheritance never changes the contract aspects of a subprogram body.

That clearly works well on the body side of the contract; if the contracts
changed with inheritance, it would be much harder to figure out what properties
can be depended upon (or have to be preserved in the results).

OTOH, it doesn't seem to work as well on the call side of the contract. The
current rules say that the contracts depend on the actual body executed; the
implementation is likely to be a wrapper around the "regular" body (if the
contracts are normally enforced at the call site).

This has some unfortunate effects when interfaces are "added" into an existing
type hierarchy. For example, consider:

    package P1 is
       type T1 is tagged private;
       function Is_Valid (Obj : T1) return Boolean;
       procedure P1 (Obj : in out T1);
    private
       ...
    end P1;

    package P2 is
       type I2 is interface;
       function Is_Wobbly (Obj : I2) return Boolean is abstract;
       procedure P1 (Obj : in out I2) is null
           with Post'Class => Is_Wobbly (I2);
       procedure P2 (Obj : in I2) is null
           when Pre'Class => Is_Wobbly (I2);
    end P2;

    with P1, P2;
    package P3 is
       type T3 is new P1.T1 and P2.I2 with private;
       overriding
       function Is_Wobbly (Obj : T3) return Boolean;
       overriding
       procedure P2 (Obj : in T3);
    private
       ...
    end P3;

    with P1, P3;
    procedure Main is
        procedure Do_It (Obj : in P3.T3'Class) is
        begin
           Obj.P1; -- (1)
           Obj.P2; -- (2)
        end Do_It;
        O3 : P3.T3;
    begin
        Do_It (O3);
    end Main;

The dispatching call to P1 at (1) will call P1.P1, inherited from type T1.
This P1 has no postcondition, so Is_Wobbly will not be called on exit from P1.
However, the following call to P2 at (2) will call P3.P2; it will inherit the
precondition from the interface. Thus Is_Wobbly will be called on entrance to
P2. If P1 returned a value for which Is_Wobbly is False (perhaps because the
programmer forgot to override P1 for type T3), the *precondition* on the call to
P2 would fail. But that is bizarre; given the postcondition matches the
precondition for the type of the calls, it will be totally mysterious to the
programmer as to why the failure is there. The only way to reason about these
calls is to know the details of the contracts for all of the various possible
routines involved -- that way seems to lead to madness! (And of course the code
will most likely not be this easy to analyze).

It is of course possible to create similar examples with the Type_Invariant
aspect.

These examples bother me so much simply because here we have a contract that we
appear to be promising to enforce, yet we aren't enforcing it. Lying to the
client (whether or not there is some logical reason for it) does not seem like a
good policy.

This is just one effect of these rules. More generally, these rules prevent any
analysis of the contracts of a dispatching call -- by the programmer, by the
compiler, or by any tool that doesn't have access to the complete source code of
the program. That's because even if the entire program obeys a programming style
rule to avoid the "funny" cases, a subprogram that hasn't even been written yet
can add additional contracts (via any of the class-wide or specific contract
aspects) -- and those would render any analysis wrong.

One side effect of this that generating the contract aspects at the point of the
call is not possible in general. That of course means that the compiler cannot
eliminate checks of those aspects when they are not needed, nor point out when
they are guaranteed to fail. It also means that wrappers are needed for the
dispatching versions of routines if the compiler generates such aspects at the
call site for statically bound calls.

The rules for combining contracts (especially preconditions) also seem confusing
at best. Adding a precondition to an overriding routine causes a *weaker*
precondition; the original class-wide precondition no longer needs to be true.
That does not seem helpful and surely makes analysis harder.

All of these rules seem to vary from the usual model of dispatching calls. For
instance, constraints can be thought of a weaker form of contract aspects (as
preconditions involving only a single parameter, for instance). Ada 95 required
constraints to match exactly (3.9.2(10/2) requires subtype conformance) for
routines that override inherited routines (that is, possible dispatching
targets). (Ada 2012 will of course extend this to subtype predicates.) Ada also
has similar rules for other properties (including Convention, also in
3.9.2(10/2), and the No_Return aspect (6.5.1(6/2))). It would have had similar
rules for global in/global out annotations had those been defined, and most
likely would have similar rules for exception contracts as well.

So why should contract aspects (Pre/Post/Type_Invariant) be different? If these
are considered part of the profile, with suitable rules all of the bizarre cases
go away.

The easiest rule would be to require (full) conformance of contract aspects that
apply to a subprogram. Effectively, only one (class-wide) precondition could
apply to a dispatching call - the same precondition would apply to all of the
subprograms that could be dispatched to. This sounds very limiting, but as
Tucker has pointed out, such a precondition could be made up of other
dispatching calls. (Sorry Tucker for using your argument against you... :-)

If we were to make such aspects part of the profile, then it would seem that we
should have similar requirements on access-to-subprogram types. That would not
be strictly necessary, but note that the same sorts of issues apply to calls
through access-to-subprogram types. These bother me far less (especially as
wrappers might be required to deal with access-before-elaboration checks), but
consistency seems valuable.

We could use other somewhat weaker rules. One thing that bothers me about the
"absolute" rule is that a lot of potentially dispatching routines are never
called that way in practice. Such routines could have conventional specific
contract aspects without problems.

One could even imagine using Tucker's original rules (although that leaves
Steve's problem unsolved) so long as there is the possibility of compile-time
enforcement of a stricter rule so that at least "well-structured" dispatching
calls could have their properties known at the call site.

For me, the most important part of contract aspects is that they are known at
the call site. This opens up the possibility of the compiler eliminating the
checks (and even more importantly, warning when the contracts are known to fail)
without having to know anything about the implementation of the subprogram.
Denying this possibility to dispatching calls makes such calls a second-class
citizen in the Ada universe, and reduces the contract aspects to little more
than fancy Assert pragmas (only Type_Invariant does much automatically).

Thus I think we need to reconsider this area. (As a side effect, such
reconsideration may very well eliminate the problem that Steve was trying to
fix.)

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

From: Tucker Taft
Sent: Friday, March 4, 2011  9:43 AM

After thinking more about this, I now agree with Randy that we have a problem.
It arises whenever an operation inherited from an interface is overridden with
an operation inherited from some other type.  My conclusion is that it may be
necessary for a new version of the inherited routine to be generated, so that
the compiler can insert the additional checks implied by Pre'Class, Post'Class,
etc. aspects inherited from the interface.

This breaks the principle that you can always just reuse the code when you
inherit an operation, but I believe in the presence of multiple inheritance of
class-wide aspects, we don't really have a choice.

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

From: Randy Brukardt
Sent: Friday, March 4, 2011  9:46 PM

I'm happy to hear that; I'd hate to think that I was making less sense than
Charlie Sheen...

However, I don't think this quite works, because of the "weakening" rules for
preconditions. The new precondition inherited from the interface could
"counterfeit" the precondition on the original body, leading to a scenario where
the body is called without problem with parameters that violate the precondition
that it knows about. That seems pretty nasty.

To give a specific example:

    package P1 is
       type T1 is tagged private;
       function Is_Valid (Obj : T1) return Boolean;
       procedure P (Obj : in out T1)
          with Pre'Class => Is_Valid (Obj);
    private
       ...
    end P1;

    package body P1 is
       procedure P (Obj : in out T1) is
       begin
          -- Code here that assume Is_Valid is True for Obj.
       end P;
    end P1;


    package P2 is
       type I2 is interface;
       function Is_Wobbly (Obj : I2) return Boolean is abstract;
       procedure P (Obj : in out I2) is null
           with Pre'Class => Is_Wobbly (I2);
       function Something_Wobbly return I2
           when Post'Class => Is_Wobbly (Something_Wobbly'Result);
    end P2;

    with P1, P2;
    package P3 is
       type T3 is new P1.T1 and P2.I2 with private;
       overriding
       function Is_Wobbly (Obj : T3) return Boolean;
       overriding
       function Something_Wobbly return T3;
    private
       ...
    end P3;

    with P1, P3;
    procedure Main is
        procedure Do_It (Obj : in P3.T3'Class) is
        begin
           Obj.P; -- (1)
        end Do_It;
    begin
        Do_It (P3.Something_Wobbly);
    end Main;

Using the new semantics Tucker suggested, the call at (1) has to pass its
precondition, as Is_Wobbly(Obj) has to be true (based on the postcondition of
Something_Wobbly). However, since preconditions are effectively combined with
"or", Is_Valid(Obj) might in fact be False. And if it is, the body of P is going
to be mighty surprised to get an object that violates its precondition!

(I don't think this problem happens for Post or Type_Invariant, as they are
"anded", nor would it happen if the precondition was described as a
Dynamic_Predicate.)

Also note that this "weakening" means that even Pre'Class that necessarily must
apply to all calls cannot be generated at the call-site (because of the possible
need to "or" it with some other precondition) -- which eliminates the ability of
the compiler to do much in the way of checking elimination. (Again, this is not
a problem with the other aspects.)

It seems that "weakening" doesn't apply to multiple inheritance as much as it
does to the "primary" inheritance. But that doesn't seem to lead to a rule that
makes much sense, as it would seem to treat progenitors different than interface
parents (something we've avoided in the past).

The easy fix would be to combine the preconditions with "and". But I realize
there are logical issues with that on the call side of the equation. It strikes
me that there are logical issues on one side or the other whenever contract
aspects are combined; they only make sense if there is only one.

Thus a radical solution would be to require that exactly one precondition apply
to each subprogram (either Pre or Pre'Class, possibly inherited). To support
combining and "weakening", we'd need a way to refer to the aspects of a parent
routine, so that they can be used in a new Pre aspect. An attribute would work,
something like: P'Parent_Pre.

That would mean that you couldn't change Pre'Class precondition; if you need to
do that, you'd have to use a Pre on each subprogram in the inheritance. Not sure
if that is too complicated. And you couldn't assume much about the calls if you
did that (rather than using a single Pre'Class), but as that is the current
state, I can hardly imagine that it is harmful.

Anyway, more thought is needed.

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

From: Jean-Pierre Rosen
Sent: Saturday, March 5, 2011  1:26 AM

> Using the new semantics Tucker suggested, the call at (1) has to pass
> its precondition, as Is_Wobbly(Obj) has to be true (based on the
> postcondition of Something_Wobbly). However, since preconditions are
> effectively combined with "or", Is_Valid(Obj) might in fact be False.
> And if it is, the body of P is going to be mighty surprised to get an
> object that violates its precondition!

Doesn't Eiffel have the same problem? How is it handled? (Just trying to avoid
reinventing the wheel).

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

From: Randy Brukardt
Sent: Saturday, March 5, 2011  2:14 AM

I had wondered the same thing, but am not sure if Eiffel has interfaces or some
other form of multiple inheritance. (Without that, this particular problem
cannot come up.)

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

From: Bob Duff
Sent: Saturday, March 5, 2011  7:32 AM

Eiffel has multiple inheritance.  Not just interfaces -- you can inherit two
non-abstract methods that conflict, and there's some syntax for resolving the
conflict (combine them into one, rename one or both, ....).

I haven't had time to understand the issue you guys are talking about, so I
don't know how it relates to Eiffel.

One possibly-related thing is that in Eiffel preconditions are checked by the
caller ("as if", of course).

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

From: Tucker Taft
Sent: Saturday, March 5, 2011  10:28 AM

Eiffel has full multiple inheritance.

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

From: Jean-Pierre Rosen
Sent: Saturday, March 5, 2011  11:26 AM

> I had wondered the same thing, but am not sure if Eiffel has
> interfaces or some other form of multiple inheritance. (Without that,
> this particular problem cannot come up.)

Eiffel has full multiple inheritance (Bertrand Meyer has claimed that no
language is usable without full multiple inheritance - but that was before
interfaces)

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

From: Tucker Taft
Sent: Thursday, March 17, 2011  3:30 PM

Eiffel essentially follows the same rules we have proposed for Ada 2012, though
it requires slightly different syntax when augmenting a precondition in a
descendant type.

Rather than saying simply "requires X > 0" to establish a precondition, you say
"requires else X > 0" to emphasize that the new precondition is tacked onto any
inherited precondition with an "or else."  Similarly, to define a postcondition,
you write "ensures Y > 0", but to "override" one you write "ensures then Y > 0",
emphasizing that this is tacked on using "and then."  I can't say I find
"requires else" or "ensures then" palatable from an English point of view, but
it is comforting to know they have adopted the implicit "or-ing"/"and-ing"
approach.

In an earlier version of Eiffel, they allowed overriding and merely established
the principle that the programmer should only write weaker preconditions, and
stronger postconditions, but made no effort to check that.  In the current
version, there is no way to write a stronger precondition, or a weaker
postcondition, because of the implicit "or-ing"/"and-ing" semantics.

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

From: Tucker Taft
Sent: Thursday, March 17, 2011  3:35 PM

Here is a web page that defines some of this for Eiffel:

   http://docs.eiffel.com/book/method/et-inheritance#Inheritance_and_contracts

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

From: Bob Duff
Sent: Thursday, March 17, 2011  7:10 PM

Thanks, Tuck.

Here's another possibly-interesting web site about Eiffel, which I have not
read, but I noticed the interesting statement, "Assertions can be statically
verified":

    http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/modern_eiffel.txt

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

From: Tucker Taft
Sent: Thursday, March 17, 2011  9:13 PM

Interesting.  It looks like things went quiet about 18 months ago.  Their
concept of static verification is pretty simplistic.

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

From: Randy Brukardt
Sent: Saturday, March 19, 2011  7:45 PM

> Eiffel essentially follows the same rules we have proposed for Ada
> 2012, though it requires slightly different syntax when augmenting a
> precondition in a descendant type.

It occurred to me this morning (in thinking about an off-hand remark that Bob
made) that we're looking at the wrong part of the problem. It's not the
combining that is getting us in trouble, it is the thinking about how these
things are enforced.

These contract aspects (Pre/Post/Type_Invariant) are visible to callers and form
part of the contract of the call. I started musing about what would happen if we
formally stated that they belong to the call (and are generated at the call
site) rather that to the called body. And I realized that most of the problems
go away; moreover, the weakening/strengthening makes much more sense.

The question is what are these contracts intended to do? If we consider the
purpose to be ensuring correctness of calls, then this focus makes perfect
sense.

Note that for normal, statically bound calls, there is no difference between
considering the call or the body. But for dispatching calls, there is an obvious
difference -- only that part of the contract aspects needed to ensure the
caller's correctness are enforced. (If it is needed to enforce something on all
calls to a particular body, it shouldn't be in a contract aspect; we have
assertions and predicates for that.)

What's interesting is that we don't *need* to enforce all of the contract
aspects in order for a body to have a consistent view of its callers. The
"weakening" of preconditions and "strengthening" of postconditions has the
correct effect, without the "counterfeiting" that occurs in the current rules.

To see what I'm talking about, we need to look at an example:

    package Simple_Window is
        type Root_Win is tagged ...

        function Is_Valid (Win : in Root_Win) return Boolean;

        function Create (Data : in Data_Type'Class) return Root_Win
           with Post'Class => Is_Valid (Create'Result);

        procedure Show_Hidden (Win : in out Root_Win)
           with Pre'Class => Is_Valid (Win),
                Post'Class => Is_Valid (Win);

        procedure Close (Win : in out Root_Win)
           with Pre'Class => Is_Valid (Win),
                Post'Class => not Is_Valid (Win);

    end Simple_Window;

    package Visibility is
        type Visible is interface;

        function Is_Visible (Obj : in Visible) return Boolean is abstract;

        procedure Show_Hidden (Obj : in out Visible)
            with Pre'Class  => not Is_Visible (Obj),
                 Post'Class => Is_Visible (Obj) is abstract;

        procedure Hide_Visible (Obj : in out Visible)
            with Pre'Class  => Is_Visible (Obj),
                 Post'Class => not Is_Visible (Obj) is abstract;

    end Visibility;

    with Simple_Window, Visibility; use Simple_Window, Visibility;
    package Visible_Window is
        type Visible_Win is new Root_Win and Visible with ...

        --Inherits:
        --   function Is_Valid (Win : in Visible_Win) return Boolean;

        function Is_Visible (Obj : in Visible_Win) return Boolean;

        function Create (Data : in Data_Type'Class) return Visible_Win
           with Post'Class => Is_Visible (Create'Result);
           -- This is "and"ed with Is_Valid (Create'Result).

        --Inherits:
        -- procedure Show_Hidden (Win : in out Visible_Win);

        procedure Hide_Visible (Win : in out Visible_Win)
            with Pre'Class  => Is_Valid (Win),
                 Post'Class => Is_Valid (Win);

        --Inherits:
        --procedure Close (Win : in out Root_Win);

    end Visible_Window;

    with Simple_Window, Visibility, Visible_Window;
    use  Simple_Window, Visibility, Visible_Window;
    procedure Testing is

        procedure Hide (Win : in out Visible'Class) is
        begin
            if Is_Visible (Win) then
                Hide_Visible (Win); -- (1)
            end if;
        end Hide;

        A_Win : Visible_Win := Create (...);
    begin
        if Something then
            Hide_Visible (Win); -- (2)
            Close (Win); -- (3)
        else
            Hide (Win); -- (4)
            Close (Win); -- (5)
        end if;
    end Testing;

The effect of the rules that I'm suggesting is that the details of contract
aspects that are evaluated depends upon the call.

Specifically, for the dispatching call (1), the precondition is Is_Visible
(Win), as that is the class precondition for routine being called (procedure
Hide_Visible (Obj : in out Visible'Class);). [Dispatching calls never would
evaluate specific preconditions, only the ones that apply to all of the
subprograms.] Note that whether Is_Valid (Win) is True has no effect here; that
makes sense because this is an object of Visible'Class and it doesn't even have
Is_Valid. Why would the caller care about the value of some routine that it does
not know about?

Similarly, the call (1) only checks the postcondition (not Is_Visible (Win)). No
check need be performed on other postconditions of the body.

Note the contrast with the statically bound call at (2): this evaluates the
entire precondition of the routine (Is_Valid (Win) or Is_Visible (Win)).

Note that these calls call the *same* body, but use *different* preconditions.
This seems bad. But it is not, because preconditions are "or"ed together. Thus,
inside of the body, the precondition has the same state either way (if
Is_Visible is True, then the precondition is satisfied).

Another objection might be that later callers might depend on the unchecked
Is_Valid postcondition. But look at the two calls (3) and (5). Both of these
calls (obviously) have the precondition of Is_Valid (Win). But in the case of
call (2), the postcondition of the call includes Is_Valid (Win) [so the
precondition succeeds], while the postcondition of call (4) does not (and
cannot: Visible'Class does not contain a Is_Valid operation). So there is no
reason to depend upon that value to be true. Moreover, it will be enforced
before call (5), so there is no problem even if it somehow gets False.

A final objection is that readers might treat these contract aspects as if they
are assertions and presume that they are always checked. But that seems to be
more an error of understanding than anything else; once users realize that it is
the call that matters, not the body, it will make more sense.

Note that what this rule does is make the preconditions on a dispatching call
*stronger* than those on the called body -- indeed they are strong enough so
that all possible bodies will pass. Similarly, the postconditions and invariants
on a dispatching call are *weaker*, weak enough so that call possible bodies
will pass. This almost makes sense. ;-)

---

We should now turn to the inheritance issues that lead to this discussion in the
first place.

Imagine that there is a call to Show_Hidden that immediately follows call (1).
[Not very useful, but bear with me...] The precondition for that call would be
not Is_Visible (Win). The call would dispatch to the body for the root type,
which as a precondition of Is_Valid (Win). That does seem good; at this point
the reader is probably saying, "see I knew this idea was nuts; I wish I hadn't
read this so far". Ah, but not so fast.

Let's back up a moment and imagine a version of Ada with no inheritance, only
overriding. We'd have to write the body of this routine explicitly in this case.
What would it look like? Probably something like:

     procedure Show_Hidden (Obj : in out Visible_Win) is
     begin
         Show_Hidden (Root_Win (Obj));
     end Show_Hidden;

So what, you are probably saying. Well, I see a call here -- a statically bound
call for that matter! Such a call will obviously enforce the pre and post
conditions of the called subprogram. So the missing Is_Valid (Win) call would
occur within the body of the subprogram. Since this is stronger than the
precondition of the subprogram as a whole (Is_Valid or (not Is_Visible)), it
will have to be evaluated, and thus the parent's precondition will be enforced.

So, all we have to do to avoid the "wrong precondition" problem is to treat
inherited routines where there are new contract aspects in the same way as this
call. That's not much different than the wrapper model that was previously
proposed to "fix" this case.

---

Having shown that making contract aspects apply to the call rather than to the
body eliminates the logical inconsistencies that otherwise arise, let's look a
number of smaller issues.

First, this model doesn't appear to extend that well to access-to-subprogram
types. But actually it does. Access-to-subprogram types themselves do not have
an associated contract; effectively it is true. If we apply the same rule to
'Access that we apply to inheritance, we realize that any subprogram with a
contract aspect needs a wrapper in order that that aspect gets evaluated on the
call (just like any inherited routine that *changes* a contract needs a
wrapper). This essentially is the same model as used by the existing proposal,
it would just be worded differently.

Second, there is Steve's problem of inheritance of multiple null procedures
(with different contract aspects) where an arbitrary one is called. The
"natural" model would be that a call to an arbitrary one of the routines is
generated. But that means it would be arbitrary as to what contracts are
evaluated. That doesn't seem good. But turning back to the model of "what would
we write explicitly" solves the problem. If we explicitly wrote such a body, it
almost certainly would be a null procedure itself -- we wouldn't call *any*
inherited routine. So all we have to do is write the rules so that happens (and
it is only necessary when the contracts are changed), and the question is
answered.

Third, Type_Invariant is interesting. In general, this scheme works because
preconditions are weakened and postconditions are strengthened. Thus there is no
issue with outbound invariant checks. Inbound invariant checks, however, might
cause problems in that not all of them my be evaluated. I recall that Tucker's
original invariant proposal had no inbound checks, which means that that
proposal would not have any problem. I would suggest that we consider going back
to that proposal.

This last issue reminds me that the reason that those inbound checks were added
was to detect errors earlier. This is the same reason that we wanted to ensure
that all of the preconditions and postconditions of a body are evaluated. But it
should be clear by now that doing so also breaks the logical consistency of the
checks, leading to "counterfeiting" of preconditions and/or failure to check
postconditions for the types involved in a call. If we have to make a choice
between correctness and easier debugging, I know which one I want to choose. :-)

[It should be noted that making extra postcondition checks appears to harmless
in this scheme; the problems really appear with the preconditions. But I haven't
thought about this in detail.]

Finally, this scheme has the distinct advantage that checks can be generated at
the call site. (Indeed, they have to be for preconditions of dispatching calls,
since the precondition of the call is in general stronger than the precondition
of the called body.) That exposes the checks to the full machinery of compiler
optimization, which should allow many of them to be eliminated. (And ones that
have to fail to generate warnings - even more valuable for correctness.) Since
this is existing machinery in all compilers that I know of, we want to be able
to take advantage of that.

To summarize, by changing the locus of contracts from callable entities to the
calls themselves, we eliminate the logical problems that we encounter when the
contracts belong to bodies rather than calls. Again, note that this change has
no effect for any statically bound calls, nor for access-to-subprogram calls; it
only affects dispatching calls. I think we need to look very seriously at
whether this approach works better than the body-oriented approach (even though
there is a slight cost in debugging information).

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

From: Bob Duff
Sent: Sunday, March 20, 2011  5:05 AM

> These contract aspects (Pre/Post/Type_Invariant) are visible to
> callers and form part of the contract of the call.

Yes.  But why does everybody leave out predicates, which are the most important
of the 4 new "contract" features?

>...I started musing about what would
> happen if we formally stated that they belong to the call (and are
>generated  at the call site) rather that to the called body.

Preconditions belong to the call site.  Postconditions belong to the body.

> The question is what are these contracts intended to do? If we
> consider the purpose to be ensuring correctness of calls, then this
> focus makes perfect sense.

The purpose of preconditions is to ensure the correctness of calls.
In order to prove a precondition correct (either by hand, or using some tool),
you typically need to look at the actual parameters.  Postconditions are the
flip side -- they're supposed to be true for ANY call.

Sorry, but your e-mail is too long for me to read right now.
I'll try to get to it later.  I'm definitely interested!

I think there's a bug in the rules that prevents preconditions from being
checked at the call site.  This came up in a discussion that Cyrille Comar was
involved in, and then the discussion got dropped on the floor before anybody
figured out what the problem is.

I'd rather spend energy on getting this stuff right, rather than
(say) obscure corners of the accessibility rules that apply only to programs
that nobody writes.  ;-)

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

From: Tucker Taft
Sent: Sunday, March 20, 2011  7:23 AM

     Thanks for this nice explication.
I actually agree with you that the right "view" is from the caller -- that is
really what preconditions and postconditions are about.  One of our goals,
however, was that the preconditions could be *implemented* by doing the correct
check inside the called routine. That will generally be less time efficient, but
it is clearly more space efficient, and for some compilers might simplify
implementation.  However, if we keep your "caller" view clearly in sight, it
becomes apparent that for inherited code, this may not work, and a new version
of the code that performs a weaker precondition check and a stronger
postcondition check will be needed. So it isn't even a "wrapper."  It really
needs to be a new version, or perhaps an "unwrapper" which bypasses the stronger
precondition check in the inherited code.

But you are right, the semantics are simpler to understand, and the "funny"
inheritance rules make more sense, if in the RM we define the semantics from the
caller side.  We should still make some effort in my view to allow the body-side
implementation of checks if desired, but the caller side view should remain the
underlying semantics.

By the way, Bob implied that postconditions were to be associated with the body.
I don't agree.  Postconditions are both more time *and* space efficient if
performed inside the body, but the right semantic view is still from the
caller's point of view.  Preconditions and postconditions are promises made to
the *caller*.  Also, there is no guarantee that the postconditions are the same
for every call, since they could depend on the value of the IN parameters. E.g.,
the postcondition of "max" is clearly dependent on the values of the IN
parameter (e.g. Max'Result >= Left and Max'Result >= Right and (Max'Result =
Left or Max'Result = Right))

Access-to-subprogram is admittedly weird, and I'm not sure what we should do
with those.  Since we don't seem motivated to put pre/postconditions on
access-to-subp types, the question is what if any preconditions can/should be
enforced in the body. Based on the caller view, the answer would be *none*.
However, that pretty much defeats the ability to implement body-side checks.
Hence, we have proposed that the preconditions *are* checked.  But this is after
all of the "or"ing has taken place with inherited 'Class preconditions.

So perhaps a way to think about it is that on a call through an access-to-subp
value, a precondition is checked that is the "or" of every possible
non-access-to-subp call.  Another way to look at is that a subprogram reached
through an acc-to-subp indirection can still act as though it was called
directly in some way, including potentially a dispatching call if it is a
dispatching operation. It need not worry about the access-to-subp possibility.
Yet another way to think about it is that an access-to-subp call is actually a
call on a wrapper that contains a "normal" call, so we know that *some*
precondition check is performed, depending on which sort of "normal" call is
chosen to be used inside this wrapper.

In any case, I think we are in agreement that the caller view is the key to
understanding the semantics for preconditions and postconditions.  Type
invariants are more like postconditions in my view, and so are a bit easier to
reason about.  Subtype predicates are really more associated with subtype
conversions, and subtype conversions clearly happen on the caller side as far as
parameters and results, since the body doesn't really have any clue as to the
subtypes of the actual parameters or the target of the return object.

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

From: Yannick Moy
Sent: Monday, March 21, 2011  12:36 PM

> So, all we have to do to avoid the "wrong precondition" problem is to
> treat inherited routines where there are new contract aspects in the
> same way as this call. That's not much different than the wrapper
> model that was previously proposed to "fix" this case.

Could you point me to the discussions about the "wrong precondition" problem? Or
was it only discussed at ARG meetings?

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

From: Tucker Taft
Sent: Monday, March 21, 2011  12:45 PM

The problem is related to inheriting a subprogram from the parent type with a
particular precondition, while also inheriting abstract or null subprograms from
one or more interface "progenitors" that have different preconditions but
otherwise match the subprogram inherited from the parent.

The danger is that the inherited code will enforce the precondition it had in
the parent, when in fact it should also "or" in the preconditions coming from
the interface progenitor (effectively weakening the precondition).

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

From: Randy Brukardt
Sent: Monday, March 21, 2011  9:59 PM

> > These contract aspects (Pre/Post/Type_Invariant) are visible to
> > callers and form part of the contract of the call.
>
> Yes.  But why does everybody leave out predicates, which are the most
> important of the 4 new "contract" features?

Because they don't have anything to do with subprograms, and in particular have
nothing to do with any of the problem cases.

This discussion started originally because of a question that Steve had about
inheriting null procedures that had different contract aspects, and eventually
widened into a question about any inheritance that causes different contract
aspects.

Such inheritance cannot happen for predicates. When you have any form of
inheritance, all of the inherited and overriding routines must be subtype
conformant. That requires static matching for any subtypes, and that requires
the predicates to be exactly the same.

Since the predicates have to be the same for any possible body that a
dispatching call might execute, there is no issue to discuss. Thus I've left any
mention of predicates out of my messages, since that would just confuse the
issue further.

[Note that the solution that makes predicates have no problems could also be
used for other contract aspects -- that is, requiring them to be the same
everywhere -- but that seems to be a fairly limiting solution.]

> >...I started musing about what would
> > happen if we formally stated that they belong to the call (and are
> >generated  at the call site) rather that to the called body.
>
> Preconditions belong to the call site.  Postconditions belong to the
> body.

That's wrong; Tucker explained why. If you take this literally, you could never
use the postconditions to prove and eliminate following preconditions -- which
would be silly.

...
> I think there's a bug in the rules that prevents preconditions from
> being checked at the call site.  This came up in a discussion that
> Cyrille Comar was involved in, and then the discussion got dropped on
> the floor before anybody figured out what the problem is.

It's not a bug, as Tucker points out, it was completely intended. It's just
completely wrong -- the rules should be that preconditions are *always* checked
at the call site, and then if the compiler can and wants to do some as-if
optimizations, that's fine.

> I'd rather spend energy on getting this stuff right, rather than
> (say) obscure corners of the accessibility rules that apply only to
> programs that nobody writes.  ;-)

Feel free. :-)

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

From: Randy Brukardt
Sent: Monday, March 21, 2011  10:22 PM

>      Thanks for this nice explication.
> I actually agree with you that the right "view" is from the caller --
> that is really what preconditions and postconditions are about.  One
> of our goals, however, was that the preconditions could be
> *implemented* by doing the correct check inside the called routine.

And this is where we went off the rails. This is an *optimization*; we must not
break the logical rules in order to make this possible. And I think I've
convinced myself that this is not possible in general (although it is possible
for any subprogram that cannot be called with a dispatching call -- and there
are a lot of those in typical Ada programs).

> That will generally be less time efficient, but it is clearly more
> space efficient, and for some compilers might simplify implementation.
> However, if we keep your "caller" view clearly in sight, it becomes
> apparent that for inherited code, this may not work, and a new version
> of the code that performs a weaker precondition check and a stronger
> postcondition check will be needed.
> So it isn't even a "wrapper."  It really needs to be a new version, or
> perhaps an "unwrapper" which bypasses the stronger precondition check
> in the inherited code.

The important point that I picked up on is that the preconditions that are
enforced for a dispatching call ought to be those that apply to the routine that
the call resolves to, and not those of the actual body.

For consistency, I suggested that we apply that to all of the contract aspects,
but it would work fine to apply that only to preconditions.

> But you are right, the semantics are simpler to understand, and the
> "funny" inheritance rules make more sense, if in the RM we define the
> semantics from the caller side.  We should still make some effort in
> my view to allow the body-side implementation of checks if desired,
> but the caller side view should remain the underlying semantics.

I think we should allow body side implementation by making sure that we don't
specify precisely where the exception is raised; but if the results are
different (as in dispatching calls), then it is up to compilers to get the right
result.

> By the way, Bob implied that postconditions were to be associated with
> the body.  I don't agree.  Postconditions are both more time *and*
> space efficient if performed inside the body, but the right semantic
> view is still from the caller's point of view.  Preconditions and
> postconditions are promises made to the *caller*.  Also, there is no
> guarantee that the postconditions are the same for every call, since
> they could depend on the value of the IN parameters.
> E.g., the postcondition of "max" is clearly dependent on the values of
> the IN parameter (e.g. Max'Result >= Left and Max'Result >= Right and
> (Max'Result = Left or Max'Result = Right))

I agree, although I don't really agree that they are necessarily more time and
space efficient. It seems to me to be necessary to consider the complete
picture. If you put postconditions into the body, your optimizer might be able
to prove that some of the checks aren't needed. But if you do that, you can no
longer prove that some of the following *preconditions* are no longer needed. So
whether the result is more time-efficient or not is very unclear to me.

You might be able to do better if you have some way to inject the values of
"virtual expressions" into your intermediate form after calls. [This is, somehow
tell the optimizer that the values of the post-condition expressions are known.]
I don't know if optimizers typically have this ability; our optimizer definitely
does not (and I don't know if this idea has a name; I doubt that I am the first
to think of it!). But doing that is not much different from the ability to
generate the postcondition at this point (since these are arbitrary
expressions).

[Note that I'm mostly interested in what can be done with existing or common
compiler technology. If you generate both the pre and post conditions at the
call site, typical common-subexpression optimizations will remove the vast
majority of the precondition checks, since they will be satisfied by preceeding
postconditions. Moreover, if the optimizer determines that some precondition is
always going to be False, a compile-time warning could be issued that there is
an obvious bug in the program.

"Virtual expressions" would use the same mechanism that common subexpressions do
(especially for determining whether it is OK to treat two similar expressions as
always getting the same result), other than inserting a known static value
rather than evaluating into a temporary. (And you'd have to be careful not to
use part of one in other optimizations, since they wouldn't actually be
evaluated there.)]

> Access-to-subprogram is admittedly weird, and I'm not sure what we
> should do with those.  Since we don't seem motivated to put
> pre/postconditions on access-to-subp types, the question is what if
> any preconditions can/should be enforced in the body.
> Based on the caller view, the answer would be *none*.
> However, that pretty much defeats the ability to implement body-side
> checks.  Hence, we have proposed that the preconditions *are* checked.
> But this is after all of the "or"ing has taken place with inherited
> 'Class preconditions.
>
> So perhaps a way to think about it is that on a call through an
> access-to-subp value, a precondition is checked that is the "or" of
> every possible non-access-to-subp call.  Another way to look at is
> that a subprogram reached through an acc-to-subp indirection can still
> act as though it was called directly in some way, including
> potentially a dispatching call if it is a dispatching operation.
> It need not worry about the access-to-subp possibility.
> Yet another way to think about it is that an access-to-subp call is
> actually a call on a wrapper that contains a "normal"
> call, so we know that
> *some* precondition check is performed, depending on which sort of
> "normal" call is chosen to be used inside this wrapper.

I think you lost me. I proposed in my message that we think of an
access-to-subprogram in the same way that we think of a dispatching call to a
routine that has different contracts. Since the access-to-subprogram has no
contracts, that puts the entire contract in the body (logically). That's the
*same* idea that I suggested for inherited dispatching bodies where the
contracts are different.

> In any case, I think we are in agreement that the caller view is the
> key to understanding the semantics for preconditions and
> postconditions.  Type invariants are more like postconditions in my
> view, and so are a bit easier to reason about.  Subtype predicates are
> really more associated with subtype conversions, and subtype
> conversions clearly happen on the caller side as far as parameters and
> results, since the body doesn't really have any clue as to the
> subtypes of the actual parameters or the target of the return object.

Now for the tough question: who is going to try to take a crack at rewording the
rules in order to have the correct effects? I might have time next week, but I
think this one is going to require a number of iterations, so the sooner we
start the better.

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

From: Randy Brukardt
Sent: Monday, March 21, 2011  11:16 PM

> The problem is related to inheriting a subprogram from the parent type
> with a particular precondition, while also inheriting abstract or null
> subprograms from one or more interface "progenitors"
> that have different preconditions but otherwise match the subprogram
> inherited from the parent.
>
> The danger is that the inherited code will enforce the precondition it
> had in the parent, when in fact it should also "or" in the
> preconditions coming from the interface progenitor (effectively
> weakening the precondition).

I think this description is backwards, because you're talking about what the
inherited code will do; the point is what the *call* to it will do; the language
(even the current wording) does not talk much about what bodies do, as these
things are defined on calls more than on bodies.

The danger really is that the preconditions that are enforced will be different
(possibly weaker) than those expected by the body; *or* that the postconditions
that are enforced are different (weaker) than those expected by the caller. If
we really want to talk about these in terms of bodies, then we need different
rules for preconditions and postconditions!

Anyway, to answer Yannick's question, there are examples of the problem in my
message of Saturday (procedure Show_Hidden has the classic example of the issue,
depending on the rules for such inheritance). There are also examples in the
mail of AI05-0197-1 (which will soon be moved to the new AI05-0247-1).

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

From: Randy Brukardt
Sent: Tuesday, March 22, 2011  1:28 AM

One of the things I was thinking about is that the model of "weakening"
preconditions doesn't seem to work properly with existing code when dispatching
is involved.

Consider:

    package Pack1 is
       type T1 is tagged private;
       function Is_Valid (Obj : T1) return Boolean;
       procedure P1 (Obj : in T1);
    private
       ...
    end Pack1;


    with Pack1;
    package Pack2 is
        type T2 is new Pack1.T1 with ...
        overriding
        procedure P1 (Obj : in T2)
            when Pre'Class => Is_Valid (Obj);
    end Pack2;

Imagine that Pack1 is some existing library (say, Ada.Containers.Vector).
And Pack1 is written by a user that wants to use this new-fangled precondition
thingy.

The problem here is that the precondition of the original P1 is True. So it is
impossible to give a weaker precondition later.

However, the current wording ignores the preconditions for which none is
specified. That's probably because the alternative is to effectively not
allow preconditions at all on overriding routines. However, that does not work
at all with the model of weakening preconditions.

For example:

    with Pack1;
    procedure Do_It3 (Obj : in Pack1.T1'Class) is
    begin
        Obj.P1;
    end Do_It3;

The dispatching call Obj.P1 has no precondition. However, if Obj is a T2 object,
then the body of P1 has a *stronger* precondition.

We can handle this by requiring the precondition of the actual routine to be
evaluated in this case. Interestingly, this is the same as the requirements for
adding a precondition to an inherited via multiple inheritance; perhaps that
needs to apply any time a precondition is added?? (Nah, that's too strong. It
only needs to apply any time that the precondition might be different or
originally empty.)

In any case, an empty class-wide Precondition is different than one specified to
be True. Specifically, if the original P1 was:

        procedure P1 (Obj : in T1
            when Pre'Class => True;

then adding a later precondition on some extension would have no effect.
Whatever rules we come up with had better take this into account.

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