Version 1.3 of ai05s/ai05-0247-1.txt

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.

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

From: Tucker Taft
Sent: Tuesday, March 22, 2011  9:47 AM

I think you need to put a Pre'Class
precondition on the operations of the root type if you want any of this to work.

I suppose we could treat the "Pre" and the "Pre'Class"
preconditions completely independently, and the "Pre'Class" get weakened as you
go down the hierarchy, and the Pre are evaluated as is, and a failure of the
"Pre" is a failure, end of story, just as though the precondition were an
assertion as the first line of the subprogram body.

That way you could add Pre's anywhere, and not have to worry about your
ancestors.  They would be effectively enforced in the body.  Meanwhile,
Pre'Class would be consistently described as enforced at the call site, and
would undergo weakening.  I guess I kind of favor this model. Mixing Pre and
Pre'Class seems like a mistake in general, and I believe that projects will
adopt one approach or the other.

We would still need to think about how access-to-subp interacts with this.
Probably should still be modeled as a call on a conjured-up subprogram that
contains a normal, non-dispatching call on the designated subprogram.

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

From: Randy Brukardt
Sent: Tuesday, March 22, 2011  4:52 PM

> I think you need to put a Pre'Class
> precondition on the operations of the root type if you want any of
> this to work.

I can believe that that is preferred. But the language rules have to make sense
even when that is not done, because of compatibility concerns. There is a lot of
code out there without preconditions, and we don't want to prevent using it, or
make it hard to use preconditions.

> I suppose we could treat the "Pre" and the "Pre'Class"
> preconditions completely independently, and the "Pre'Class"
> get weakened as you go down the hierarchy, and the Pre are evaluated
> as is, and a failure of the "Pre" is a failure, end of story, just as
> though the precondition were an assertion as the first line of the
> subprogram body.

Yes, I think I suggested something on this line a week or two ago. I think it
makes more sense.

> That way you could add Pre's anywhere, and not have to worry about
> your ancestors.  They would be effectively enforced in the body.
> Meanwhile, Pre'Class would be consistently described as enforced at
> the call site, and would undergo weakening.  I guess I kind of favor
> this model.
> Mixing Pre and Pre'Class seems like a mistake in general, and I
> believe that projects will adopt one approach or the other.

I have to wonder if we shouldn't enforce that. Mixing them makes no logical
sense. (I also proposed this last week.)

Specifically, either one of Pre'Class or Pre can be specified on a subprogram.
And, for an overriding/inherited routine, Pre'Class can only be specified/added
to a subprogram if its ancestors have Pre'Class. (And if Pre'Class is inherited,
then Pre cannot be specified, only Pre'Class.)

These rules would avoid confusion with mixed Pre/Pre'Class environments.
Pre'Class works like the Eiffel contracts; Pre is more of a free-form assertion.

Pre would always just be that of the body. Pre'Class would be that of the
*call* (with the special cases for inheritance from two subprograms).

One could even consider access-to-subprogram in the same way, as a profile that
does not have a Pre'Class, meaning that subprograms with Pre'Class couldn't
match it. We could then consider adding Pre'Class/Post'Class to
access-to-subprogram, making the similarity with dispatching calls complete.

This might be going too far, but it seems that combining Pre and Pre'Class is
too confusing for everyone. We're better off without it.

> We would still need to think about how access-to-subp interacts with
> this.  Probably should still be modeled as a call on a conjured-up
> subprogram that contains a normal, non-dispatching call on the
> designated subprogram.

I've answered this repeatedly, and you don't seem to be registering my various
ideas. So I'm not sure what's wrong with them.

Anyway, it strikes me that any model separation would be on top of the existing
rules. I think I've figured out a consistent set of changes to the dynamic
semantics that fixes the issues (but I'm sure once Steve reviews it I will have
that misconception removed ;-). I think we could add some Legality Rules to it
if we wanted to seriously separate Pre and Pre'Class, but I don't think it is
required. I'll try to write it up ASAP.

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

From: Tucker Taft
Sent: Tuesday, March 22, 2011  5:05 PM

>> I suppose we could treat the "Pre" and the "Pre'Class"
>> preconditions completely independently, and the "Pre'Class"
>> get weakened as you go down the hierarchy, and the Pre are evaluated
>> as is, and a failure of the "Pre" is a failure, end of story, just as
>> though the precondition were an assertion as the first line of the
>> subprogram body.
>
> Yes, I think I suggested something on this line a week or two ago. I
> think it makes more sense.

Yes, I should have acknowledged you.  But I frequently lose track of where ideas
come from (sorry about that), and just slowly integrate them into the overall
possibilities...

>> We would still need to think about how access-to-subp interacts with
>> this.  Probably should still be modeled as a call on a conjured-up
>> subprogram that contains a normal, non-dispatching call on the
>> designated subprogram.
>
> ... I've answered this repeatedly, and you don't seem to be
> registering my various ideas. So I'm not sure what's wrong with them.

Sorry, again I am having trouble keeping track of whose ideas are whose.  Are we
in agreement on this one, namely that an access-to-subp is equivalent to a
"normal" call on the designated subprogram, with the appropriate pre or
pre'class enforced?  That is, any precondition check to be performed is bundled
into a wrapper if necessary?  Or if not, how does your idea differ?

> Anyway, it strikes me that any model separation would be on top of the
> existing rules. I think I've figured out a consistent set of changes
> to the dynamic semantics that fixes the issues (but I'm sure once
> Steve reviews it I have that misconception removed ;-). I think we
> could add some Legality Rules to it if we wanted to seriously separate
> Pre and Pre'Class, but I don't think it is required. I'll try to write it up ASAP.

Great.

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

From: Randy Brukardt
Sent: Tuesday, March 22, 2011  5:14 PM

> Yes, I think I suggested something on this line a week or two ago. I
> think it makes more sense.

Minor aside: There doesn't seem to be any rule restricting Pre'Class or
Post'Class to dispatching routines of a tagged type. It seems these are allowed
on untagged types, routines that aren't primitive, and the like. Is this
intended, or even a good idea??

    type Foo is new Integer;
    function "+" (Left, Right : Foo) return Foo
       with Pre'Class => Left > 0 and Right > 0;

    type Bar is new Foo;
    function "+" (Left, Right : Bar) return Bar;
       -- Inherits Pre'Class???

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

From: Tucker Taft
Sent: Tuesday, March 22, 2011  8:51 PM

I am pretty sure there is a restriction of 'Class aspects to tagged types or
dispatching subprograms.  Ah yes, last legality rule of AI-183:

   If the aspect_mark includes 'Class, then the associated
   entity shall be a tagged type or a primitive subprogram
   of a tagged type.

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

From: Randy Brukardt
Sent: Wednesday, March 23, 2011  8:24 PM

OK, good to find out that it is covered. But I have to admit I never thought to
look there, given that there are only a handful of such aspects and as such I
didn't expect there to be a blanket rule existing only for them. Thus, I'm not
sure that such a blanket rule is a great idea. Maybe there needs to be an AARM
note in 13.3.2 and 13.3.3 mentioning this rule.

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

From: Randy Brukardt
Sent: Wednesday, March 23, 2011  10:05 PM

It turns out that 13.3.3(6/3) repeats this rule, while there is no similar text
in 13.3.2. I marked the text in 13.3.3 as redundant (presuming no other change),
and added an AARM note to 13.3.2 for future readers that are as confused as I
was. I suspect that either the text should be deleted from 13.3.3 or something
similar added to 13.3.2 -- but I'll wait for someone other than me to make a
formal editorial change request to that effect.

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

From: Randy Brukardt
Sent: Tuesday, March 22, 2011  5:53 PM

...
>> I'll try to write it up ASAP.
>
> Great.

Hopefully this was an optimistic "great" and not the other kind. :-) Anyway,
here is version /02 of this AI, complete with a wording proposal. I didn't do
anything with legality rules (even though I think some restrictions there would
be a good idea). This seems to me to be about the minimum change to fix the
problems previously identified.

As always, comments welcome.

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

From: Randy Brukardt
Sent: Tuesday, March 22, 2011  6:10 PM

> Yes, I should have acknowledged you.  But I frequently lose track of
> where ideas come from (sorry about that), and just slowly integrate
> them into the overall possibilities...

The important point is whether we want to enforce this with Legality Rules, or
just make it the model implicitly.

I should note that we don't enforce it with Legality Rules, some subprograms can
be called both ways (from dispatching calls that expect the body to check
preconditions, and from dispatching calls are required to check the precondition
themselves). Which means that you might have to generate code in both places
(ugh). For instance:

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

    package Pack2 is
       type I2 is interface;
       function Is_Green (Obj : I2) return Boolean is abstract;
       procedure P3 (Obj : in I2) is null
           when Pre'Class => Is_Green (Obj);
    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;
       -- P3 is inherited from Pack1.P3.
    private
       ...
    end Pack3;

    with Pack1, Pack2, Pack3;
    procedure Main is
        procedure Do_It1 (Obj : in Pack1.T1'Class) is
        begin
           Obj.P3; -- (1)
        end Do_It1;
        procedure Do_It2 (Obj : in Pack2.T2'Class) is
        begin
           Obj.P3; -- (2)
        end Do_It2;
        O3 : P3.T3;
    begin
        Do_It1 (O3);
        Do_It2 (O3);
    end Main;

Call (1) is to a routine with an ordinary Precondition, so the body always
checks the precondition. Call (2) is to a routine with a Pre'Class precondition,
but the check is at the call site. But of course these call the same body, so
the body must have the code even for call (2). [That code can never fail for
call (2), even though it will be executed.]

If we made this sort of thing illegal, this could not happen.

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

From: Tucker Taft
Sent: Tuesday, March 22, 2011  6:10 PM

> !wording
>
> Change 13.3.2(19/3) from:
>
> For a dispatching call or a call via an access-to-subprogram value,
> the precondition or postcondition check performed is determined by the
> subprogram actually invoked.
> Redundant[Note that for a dispatching call, if there is a Pre'Class
> aspect that applies to the subprogram named in the call, then if the
> precondition expression for that aspect evaluates to True, the
> precondition check for the call will succeed.]
>
> to:
>
> For a dispatching call to a subprogram that does not have a Pre'Class
> specified, or a call via an access-to-subprogram value, the
> precondition or postcondition check performed is determined by the
> subprogram actually invoked. Similarly, the postcondition check for
> all dispatching calls is determined by the subprogram actually
> invoked.
>
> In contrast, the precondition check for a dispatching call to a
> subprogram that does have Pre'Class specified consists solely of
> checking the Pre'Class expressions that apply to the subprogram.

What about the "Pre" aspect?  Is this meant to imply that if there is a
Pre'Class aspect specified, then the Pre aspect is ignored?

Also, when you say the "the Pre'Class expressions that apply to the subprogram"
do you mean the subprogram denoted by the call prefix, or do you mean the
subprogram actually invoked? The wording seems ambiguous.

Finally, what are the implications that only the Pre'class known to the caller
be checked?  If one of the Pre'Class expressions that applies to the subprogram
actually invoked is True, must we still raise an Assertion_Error if all of the
expressions that apply to the denoted subprogram evaluate to False?

> AARM Ramification: We are talking about the Pre'Class that applies to
> the subprogram that the dispatching call is resolving to call, not the
> Pre'Class for the subprogram that is ultimately dispatched to.

I believe this needs to be made clearer in the normative wording.
An AARM note seems inadequate.  The word "denote" could be used to emphasize the
compile-time denoted subprogram, rather than the run-time invoked subprogram.

> AARM Implementation Note: These rules imply that logically,
> preconditions of routines that have Pre'Class specified and might be
> called with a dispatching call must be checked at the point of call.
> Preconditions of other routines that might be called with a
> dispatching call must be checked inside of the subprogram body
> (possibly in a wrapper). It's possible for both conditions to be
> necessary for routines that are inherited from multiple ancestors (in
> that case, the check at the call site necessarily be the same or
> stronger than the one inside of the routine).

I don't understand the "preconditions of other routines".  What does that mean?
Is this the "Pre" aspects as opposed to the "Pre'Class" aspects?

> In contrast, the postcondition checks always need to be
> checked
> inside the body of the routine.
> End AARM Implementation Note.
>
> Notwithstanding what this standard says elsewhere, an inherited
> subprogram that has a specified Pre'Class, Post'Class, or
> Type_Invariant'Class (see 13.3.3) and

that

> is primitive for a type that has one or more progenitors is equivalent
> to an overriding subprogram S whose body consists of:
>     * The null statement, if all of the inherited subprograms are null
> subprograms;
>     * A call on the parent subprogram, with all of the parameters the same as
>       the parameters to S (possibility with appropriate type conversions).
> If there are multiple conformant subprograms S, there is only one
> overriding subprogram S created....

Is this needed?  It feels awfully mechanistic.  Can't we accomplish this some
other way?

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

From: Tucker Taft
Sent: Tuesday, March 22, 2011  9:29 PM

> The important point is whether we want to enforce this with Legality
> Rules, or just make it the model implicitly.
>
> I should note that we don't enforce it with Legality Rules, some
> subprograms can be called both ways (from dispatching calls that
> expect the body to check preconditions, and from dispatching calls are
> required to check the precondition themselves).

The above parenthetical comment confuses me.  Should one of those said
"non-dispatching calls"?

> ... Which means that you might have to generate code in both places
> (ugh). For instance:
>
>      package Pack1 is
>         type T1 is tagged private;
>         function Is_Valid (Obj : T1) return Boolean;
>         procedure P3 (Obj : in T1)
>            with Pre =>  Is_Valid (Obj);
>      private
>         ...
>      end Pack1;
>
>      package Pack2 is
>         type I2 is interface;
>         function Is_Green (Obj : I2) return Boolean is abstract;
>         procedure P3 (Obj : in I2) is null
>             when Pre'Class =>  Is_Green (Obj);
>      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;
>         -- P3 is inherited from Pack1.P3.
>      private
>         ...
>      end Pack3;
>
>      with Pack1, Pack2, Pack3;
>      procedure Main is
>          procedure Do_It1 (Obj : in Pack1.T1'Class) is
>          begin
>             Obj.P3; -- (1)
>          end Do_It1;
>          procedure Do_It2 (Obj : in Pack2.T2'Class) is
>          begin
>             Obj.P3; -- (2)
>          end Do_It2;
>          O3 : P3.T3;
>      begin
>          Do_It1 (O3);
>          Do_It2 (O3);
>      end Main;
>
> Call (1) is to a routine with an ordinary Precondition, so the body
> always checks the precondition. Call (2) is to a routine with a
> Pre'Class precondition, but the check is at the call site. But of
> course these call the same body, so the body must have the code even
> for call (2). [That code can never fail for call (2), even though it
> will be executed.]

I'm losing you.  What do you mean by "the body must have the code even for call
(2)"?

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

From: Randy Brukardt
Sent: Wednesday, March 23, 2011  9:37 PM

> > For a dispatching call to a subprogram that does not have a
> > Pre'Class specified, or a call via an access-to-subprogram value,
> > the precondition or postcondition check performed is determined by
> > the subprogram actually invoked. Similarly, the postcondition check
> > for all dispatching calls is determined by the subprogram actually
> > invoked.
> >
> > In contrast, the precondition check for a dispatching call to a
> > subprogram that does have Pre'Class specified consists solely of
> > checking the Pre'Class expressions that apply to the subprogram.
>
> What about the "Pre" aspect?  Is this meant to imply that if there is
> a Pre'Class aspect specified, then the Pre aspect is ignored?

Yes, but not because of any explicit intent, but rather the way that Pre works.
Pre is "or"ed with all of the other Pre'Class aspects that are inherited. Since
we're using a stronger precondition on such calls than that of the invoked
subprogram, this necessarily means that any precondition of the body must
succeed. Thus there is no need to evaluate Pre in such cases; if the compiler
can prove that all calls are either this kind of dispatching calls or statically
bound calls, it can always generate the preconditions at the call site and do no
evaluation in the body. That seems like a good thing.

I was wondering whether we should even allow this mixing; that's covered in my
other e-mail which I see has a separate answer from you so I'll give it a
separate answer as well.

> Also, when you say the "the Pre'Class expressions that apply to the
> subprogram" do you mean the subprogram denoted by the call prefix, or
> do you mean the subprogram actually invoked?
> The wording seems ambiguous.

The former. I thought that it is necessary to explicitly talk about the dynamic
meaning of subprogram explicitly; anything else is necessarily static. But I
agree that it is not that clear, so if there is some better wording available,
we should use it.

> Finally, what are the implications that only the Pre'class known to
> the caller be checked?  If one of the Pre'Class expressions that
> applies to the subprogram actually invoked is True, must we still
> raise an Assertion_Error if all of the expressions that apply to the
> denoted subprogram evaluate to False?

Yes. The intent is that the stronger precondition of the call is what is
checked; that avoids "counterfeiting". If we want to be able to do analysis at
the call site (and code generation!), we have to be able to know what
preconditions and postconditions apply to that call. For postconditions, these
are "weaker" (or the same), so we need no special rules. But for preconditions,
these can be "stronger" than those of the body; in order to have any chance to
generate these at the call site, we have to be able to evaluate the "stronger"
precondition rather than the potentially weaker one of the called body.

I considered making this a permission rather than a requirement, but that only
seemed to make it harder for users to figure out what preconditions are
enforced.

Beyond that, this makes perfect sense (to me at least): the only precondition
the caller can know about for a dispatching call is the Pre'Class that applies
to the (statically) resolved subprogram. It is the one that a caller has to
conform to have a provably correct program. That being the case, why shouldn't
we also enforce it??

Note that this rule change is sort of an optimization; it is intended to allow
code generation for preconditions at the call site of dispatching calls and also
to enforce the intended (Eiffel-like) model for subprograms that have Pre'Class
aspects. We could live without it, but doing so would pretty much eliminate the
ability of compilers to optimize preconditions for dispatching calls -- that
seems bad to me. (This is the same reason that we go out of are way to allow
postconditions to be generated inside of a subprogram body -- mostly so that the
compiler can prove that they are already true and eliminate the checks.)

> > AARM Ramification: We are talking about the Pre'Class that applies
> > to the subprogram that the dispatching call is resolving to call,
> > not the Pre'Class for the subprogram that is ultimately dispatched to.
>
> I believe this needs to be made clearer in the normative wording.
> An AARM note seems inadequate.  The word "denote" could be used to
> emphasize the compile-time denoted subprogram, rather than the
> run-time invoked subprogram.

OK, I'll make an attempt to clarify up this wording. Humm, 3.9.2 uses "denotes
the declaration of a dispatching operation". But I can't quite find a way to
work "denotes" into "For a dispatching call to a subprogram that does not have a
Pre'Class specified,".

"For a dispatching call to a denoted subprogram that does not have a Pre'Class
specified,"

doesn't make much sense.

"For a dispatching call to a subprogram that does not have a Pre'Class specified
for the denoted subprogram,"

is right but way too redundant. But I can't think of anything better. I did add
a parenthetical remark to the last paragraph:

  In contrast, the precondition check for a dispatching call to a subprogram
  that does have Pre'Class specified for the denoted subprogram consists solely
  of checking the Pre'Class expressions that apply to the denoted subprogram
  (not necessarily the one that is invoked).

> > AARM Implementation Note: These rules imply that logically,
> > preconditions of routines that have Pre'Class specified and might be
> > called with a dispatching call must be checked at the point of call.
> > Preconditions of other routines that might be called with a
> > dispatching call must be checked inside of the subprogram body
> > (possibly in a wrapper). It's possible for both conditions to be
> > necessary for routines that are inherited from multiple ancestors
> > (in that case, the check at the call site necessarily be the same or
> > stronger than the one inside of the routine).
>
> I don't understand the "preconditions of other routines".
> What does that mean?  Is this the "Pre" aspects as opposed to the
> "Pre'Class" aspects?

Both "Pre" aspects, and "Pre'Class" aspects added further down the inheritance
tree. The precondition of a dispatching call is that which is known at the call
site, period. There is no advantage to weakening here, while there might be for
statically bound calls (or dispatching calls whose root is higher up the tree).

I gave the example that led to this in my other note, the one that confused you
so. I'll try to explain that again when I answer that one.

> > In contrast, the postcondition checks always need to be checked
> > inside the body of the routine.
> > End AARM Implementation Note.
> >
> > Notwithstanding what this standard says elsewhere, an inherited
> > subprogram that has a specified Pre'Class, Post'Class, or
> > Type_Invariant'Class (see 13.3.3) and
>
> that
>
> > is primitive for a type that has one or more progenitors is
> > equivalent to an overriding subprogram S whose body consists of:
> >     * The null statement, if all of the inherited subprograms are
> > null subprograms;
> >     * A call on the parent subprogram, with all of the parameters
> > the same as
> >       the parameters to S (possibility with appropriate type conversions).
> > If there are multiple conformant subprograms S, there is only one
> > overriding subprogram S created....
>
> Is this needed?  It feels awfully mechanistic.  Can't we accomplish
> this some other way?

Maybe, but I doubt it will help much. Everything I thought of always led back
here. Note that this rule is required to fix the three problems outlined in the
AARM Reason note; some solution to these problems is required. I thought that
one rule to fix all three was preferable to inventing three separate rules that
really complicate things.

As a reminder, the AARM note says:

AARM Reason: This rule eliminates three problems: (1) the issue that two null
subprograms (one of which is chosen for dispatching arbitrarily by
3.9.2(20.3/3)) may not be equivalent at runtime; (2) "counterfeiting" problems
that arise because adding an interface precondition to the mix weakens the
precondition of the inherited routine (in this case, we need to enforce the
precondition of the actual body, else it might not be true when the call is made
-- which would be bad); (3) problems that arise because postconditions and
invariants added by an interface would not be enforced on a inherited routine
(it does not know about any such contracts).

All three problems occur because of dispatching that calls inherited routines
that have a different view of the preconditions, postconditions, and invariants
that apply to them than an otherwise identical explicitly declared routine.
Besides the logical problems that arise, we also have a problem simply because
an explicitly declared routine works differently than an inherited one. That
seems bad on its face, even ignoring the other problems.

It immediately was obvious to me that there is no problem with explicitly
declared routines. That led to my original idea, which was simply to require
overriding for the problem cases - that is a nice, simple solution. That would
be a Legality Rule something like:

If the set of Pre'Class or Post'Class or Type_Invariant'Class aspects that would
apply to a call of an inherited subprogram is different than the set of
corresponding aspects of a call to the parent subprogram, then the subprogram
requires overriding.

But this rule is difficult to define properly; we don't want to talk about
"calls", really, and we don't want confusion about the implicit inherited
subprogram as opposed to the subprogram that was inherited from, and it is hard
to define "different" very well.   (Since this is a Legality Rule that requires
the programmer to do something, we don't want it to apply unless we really need
it; thus we would want to be able to prevent it from applying when the same
Pre'Class comes from multiple parents - to take one example.)

The difficulty of defining this, along with the simple fact that it requires
people to write overriding subprograms (containing calls that they could easily
make a mistake in) just to get the preconditions right caused me to look
elsewhere.

Since it is easy to define what the body of such a subprogram looks like, and
ensuring that it exists for both contract aspects and for dispatching purposes
is needed to fix the problems (in a straightforward manner), I decided to write
the proposed rules.

The best way (IMHO) to simplify these rules is to make the proposed rules apply
to *all* inherited primitive routines of tagged types -- that is, there is (for
language rule purposes) an explicit body (defined as I proposed above) for
*every* such body. Then, we could get rid of almost all of 3.9.2(20-20.3) --
only the first bullet is even possible. Compilers still can share bodies as they
do now (except in the pre/post cases of course) -- only the language definition
is changed. In that case, this rule would move somewhere else in the Standard
(3.9.2??). I didn't do this because it is a lot of language change for what is
clearly a corner case.

The alternative of trying to define these properly in place is just too hard
IHMO. The wording for each of these cases would be very complex. The problem
cases come up when there are multiple inherited routines with different
preconditions, postconditions, and the like. In those cases, the effective
aspect is the combined one. I can't figure out how to talk about that
combination, because you cannot talk about "the" inherited subprogram; there is
more than one.

And the rules themselves are complex. Specifically, the precondition for an
inherited routine called via a dispatching call is the Pre'Class of the
subprogram denoted by the call "and"ed with the actual precondition of the
parent routine. (These are often the same, but don't have to be when interfaces
are involved -- they can be completely disjoint in that case.) This is what you
would get with an explicit body, and it is best that the inherited routines work
the same way.

The precondition of a statically bound call to such an inherited subprogram is
(effectively) the precondition of the parent routine. OTOH, the postcondition of
a statically bound call is the postcondition of the parent routine "and"ed with
any postconditions inherited from other routines.

And on and on and on...

Ideas welcome, of course.

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

From: Randy Brukardt
Sent: Wednesday, March 23, 2011  9:52 PM

...
> > The important point is whether we want to enforce this with Legality
> > Rules, or just make it the model implicitly.
> >
> > I should note that we don't enforce it with Legality Rules, some
> > subprograms can be called both ways (from dispatching calls that
> > expect the body to check preconditions, and from dispatching calls
> > are required to check the precondition themselves).
>
> The above parenthetical comment confuses me.  Should one of those said
> "non-dispatching calls"?

No. If you recall from the rules I previously proposed, there are two kinds of
dispatching calls:

If the denoted subprogram has one or more Pre'Class expressions specified, then
the precondition expressed by those expressions (only) is evaluated (for
dispatching calls). These conform to the Eiffel-like model, so for the sake of
discussion, let's call them "Eiffel-like contract dispatching calls".

OTOH, if the denoted subprogram does not have a Pre'Class expressions specified,
then the precondition that is evaluated is that of the invoked subprogram; the
precondition can be anything, and reasoning about it at the call site is not
possible. Let's call these "Ad-hoc contract dispatching calls."

The question I had was whether we should enforce a separation of these two
models of contracts and calls. If we don't do that, it is possible to call the
same subprogram from both an "Eiffel-like contract dispatching call" and a
"ad-hoc contract dispatching call". As in the example that follows...

> > ... Which means that you might have to generate code in both places
> > (ugh). For instance:
> >
> >      package Pack1 is
> >         type T1 is tagged private;
> >         function Is_Valid (Obj : T1) return Boolean;
> >         procedure P3 (Obj : in T1)
> >            with Pre =>  Is_Valid (Obj);
> >      private
> >         ...
> >      end Pack1;
> >
> >      package Pack2 is
> >         type I2 is interface;
> >         function Is_Green (Obj : I2) return Boolean is abstract;
> >         procedure P3 (Obj : in I2) is null
> >             when Pre'Class =>  Is_Green (Obj);
> >      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;
> >         -- P3 is inherited from Pack1.P3.
> >      private
> >         ...
> >      end Pack3;
> >
> >      with Pack1, Pack2, Pack3;
> >      procedure Main is
> >          procedure Do_It1 (Obj : in Pack1.T1'Class) is
> >          begin
> >             Obj.P3; -- (1)
> >          end Do_It1;
> >          procedure Do_It2 (Obj : in Pack2.T2'Class) is
> >          begin
> >             Obj.P3; -- (2)
> >          end Do_It2;
> >          O3 : P3.T3;
> >      begin
> >          Do_It1 (O3);
> >          Do_It2 (O3);
> >      end Main;
> >
> > Call (1) is to a routine with an ordinary Precondition, so the body
> > always checks the precondition. Call (2) is to a routine with a
> > Pre'Class precondition, but the check is at the call site. But of
> > course these call the same body, so the body must have the code even
> > for call (2). [That code can never fail for call (2), even though it
> > will be executed.]
>
> I'm losing you.  What do you mean by "the body must have the code even
> for call (2)"?

(1) is an ad-hoc dispatching call; it requires that the precondition (Is_Valid
(Obj) or Is_Green (Obj)) is evaluated within the invoked subprogram.

(2) is an Eiffel-like dispatching call; it requires that the precondition
(Is_Green (Obj)) is evaluated at the call site. It does not need to evaluate any
other precondition, and shouldn't evaluate a precondition in the body. Luckily,
evaluating a precondition in the body has to be harmless -- the precondition of
the call has to be part of the larger precondition, and whatever part it is must
be "or"ed (and is True), so the rest is irrelevant -- but it still wastes time.

It should noted that this scenario would happen if P3 for T1 had no Pre at all,
so this is a fairly likely case in practice.

> > If we made this sort of thing illegal, this could not happen.

I hope this explains what I'm talking about here.

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

From: Tucker Taft
Sent: Wednesday, March 23, 2011  11:00 PM

> Yes, but not because of any explicit intent, but rather the way that
> Pre works. Pre is "or"ed with all of the other Pre'Class aspects that
> are inherited. Since we're using a stronger precondition on such calls
> than that of the invoked subprogram, this necessarily means that any
> precondition of the body must succeed. Thus there is no need to
> evaluate Pre in such cases; if the compiler can prove that all calls
> are either this kind of dispatching calls or statically bound calls,
> it can always generate the preconditions at the call site and do no
> evaluation in the body. That seems like a good thing. ...

I thought we were discussing the possibility of treating Pre'Class and Pre completely
independently.  That is Pre'Class is "or"ed with other Pre'Class aspects, but the
Pre aspect is not "or"ed with anything.  In other words, the Pre aspect is *always*
checked.  The Pre'Class aspect can only be weakened, thanks to the "or"-ing rules.
The Pre aspect has no such guarantee -- it acts almost exactly like an Assert pragma
placed immediately after the "is" of the body.

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

From: Randy Brukardt
Sent: Wednesday, March 23, 2011  11:52 PM

I've only considered such a separation at compile-time (via Legality Rules). That is,
a given subprogram can only have Pre or Pre'Class, never both. But since that wasn't
necessary in order to define the dynamic semantics of calls and especially the fixes
to the bugs that triggered this AI, I just defined that and was continuing to explore
whether or not the Legality Rules were a good idea.

As far as just treating them independently at runtime, that is a whole different kettle
of fish. That effectively means that the Pre and Pre'Class aspects are "and"ed together
-- which is a big change in the model. I suspect that it might in fact be a *better*
model, but it means starting over completely in thinking about all of these examples of
inheritance and the like.

One thing that immediately comes to mind is how Pre'Class is treated vis-a-vis
access-to-subprogram. One of the advantages of the model that I proposed is that
access-to-subprogram is treated the same way as a similar dispatching call (one without
a Pre'Class aspect). I don't see how that could work in the model you are suggesting;
since Pre'Class would be unknown (and thus True), it would be ignored on any
access-to-subprogram call (at least unless we allowed Pre'Class on access-to-subprogram
types). Sounds like a nasty hole.

I'm presuming that in this model, the Pre'Class aspects are "or"ed together, then the
result is "and"ed with Pre. If there is no Pre'Class, it is treated as True.

I'd hope that we continue to have the Pre'Class model as I laid out in my wording proposal
(that we use the Pre'Class of the statically identified subprogram, which is necessarily
the same or stronger than the Pre'Class of the invoked body). And then Pre of the invoked
body would be evaluated.

Please tell me if I understand your model correctly.

I'll definitely have to think about this some more.

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

From: Jean-Pierre Rosen
Sent: Thursday, March 24, 2011  1:29 AM

I think this discussion focuses too much on technical aspects, before the
principles. So here is my view of what this all means.

Pre'Class and Post'Class are the enforcement of the LSP. i.e., if B "is an" A,
then every input acceptable to an A must be accepted by a B, and every output
produced by a B must be something that could have been produced by an A. Hence
the "or" and "and" semantics.

Pre-conditions are a contract imposed on the caller. A failure of a
pre-condition is an error made by the caller. Therefore, it seems logical to
check it at the caller's site.

Post-Conditions are a promise made by the callee. Failure of a post-condition is
a flaw in the callee, therefore it seems logical to check it in the body - even
maybe at the place of the return statement, which would give the possibility to
have an exception handler in case of a failure. (AFAIR, we never discussed the
place of the check in the light of who could handle the exception).

Pre is totally different. It is a special check of a condition that must hold
for a particular subprogram, not transmitted to any one else. I agree with Tuck
that it is basically like an Assert just after the "is" of the body. It's like
explicitely checking for some special value (or combination of values) in the
body of the subprogram. I even think the latter is preferable, since you can
choose which exception is raised, so I see little value in Pre (except than the
test is performed before elaborating the declarative part of the callee).

In short, my model implies:
- Pre'class checked at the call site
- Pre, Post, and Post'class checked in the body.

(Note that the checking of Pre in the body would take care of the "anding" of
the preconditions that worried Randy).

As far as optimization is concerned, the compiler can assume that all Post and
Post'Class hold in determining if checks for Pre'Class can be eliminated.
Nothing can be done for Pre (as for an explicit check, or an Assert in the
body).

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

From: Randy Brukardt
Sent: Thursday, March 24, 2011  2:06 AM

I'm glad to hear from someone else in this discussion.

I had thought we'd already done the first principles discussion that you lay out
above; I've just been trying to fix the bugs. Apparently all of the previous
discussion is junk (since that previous model has been rejected).

Anyway, I assume that you are talking about dispatching calls in most of the
above. Pre and Pre'Class are equivalent (except for the "and"!) for statically
bound calls. Specifically, you surely can generate Pre at the call point, and
optimize it. It would be pretty bad if you couldn't. Especially as you can't
give Pre'Class on anything other than primitives of tagged types (I think I want
call-site preconditions on other subprograms!).

The current rules proposal does not allow any Pre/Post exceptions to be handled
by the body, and I think that is exactly right. Your assertion that we never
discussed it is wrong; we discussed it ad-nausem at the Tallehasse meeting (I
think you missed that one, probably why you don't know that). 13.3.2(18/3) is
pretty clear that this is the intent. The reason is that for statically bound
cases, we ought to let the compiler have the freedom to generate the checks
wherever it wants (in the body or at the call site) - in order to maximize the
possibilities for optimization/proof. Dispatching calls and access-to-subprogram
are different, of course.

I can't tell from your discussion as to exactly which Pre'Class you expect to
enforce at the call site of a dispatching call. I've proposed that it is the
statically known one, which by definition is stronger than the Pre'Class for the
actually invoked body. Is that what you are intending?? (It definitely isn't
possible to generate the code at the call site unless we specify this.)

Also, it would be helpful if you could explain in your model what you expect to
happen for calls through access-to-subprogram values to subprograms that have
Pre'Class preconditions. This seems to have to work differently than dispatching
calls, which is uncomfortable.

Finally, none of this has any effect on the actual bug fixes; the rules that
Tucker found too "mechanistic". Those rules are needed to fix bugs that only
involve Pre'Class (and Post'Class and Type_Invariant'Class); nothing about
changing the handling of Pre has anything to do with that.

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

From: Tucker Taft
Sent: Thursday, March 24, 2011  8:05 AM

> As far as just treating them independently at runtime, that is a whole
> different kettle of fish. That effectively means that the Pre and
> Pre'Class aspects are "and"ed together -- which is a big change in the
> model. I suspect that it might in fact be a *better* model, but it
> means starting over completely in thinking about all of these examples
> of inheritance and the like.

I don't think it is that big a deal, since it means you simply ignore the "Pre"
as far as inheritance, and only worry about Pre'Class. One reason I prefer this
is that it means "Pre" can be all about the code you are "protecting" with the
precondition, while Pre'Class can be about what the abstract interface requires.

Cyrille from AdaCore finds the whole Pre'Class inheritance "or"-ing thing
unpleasant, and I think there are others who might have the same view, and it
seems potentially a benefit if Pre and Pre'Class are treated independently.

Note that this doesn't come up for Post and Post'Class, since everything is
and-ed together.

> One thing that immediately comes to mind is how Pre'Class is treated
> vis-a-vis access-to-subprogram. One of the advantages of the model
> that I proposed is that access-to-subprogram is treated the same way
> as a similar dispatching call (one without a Pre'Class aspect). I
> don't see how that could work in the model you are suggesting; since
> Pre'Class would be unknown (and thus True), it would be ignored on any
> access-to-subprogram call (at least unless we allowed Pre'Class on
> access-to-subprogram types). Sounds like a nasty hole.

The model I thought we were talking about for access-to-subprogram was that you
effectively created a call at the point of the 'Access, and whatever Pre'Class
or Pre aspects that would be enforced at that point are the Pre'Class/Pre that
would be enforced at the point of any call through that access value.  That
seems very well defined, and yes, does imply a wrapper in some implementations.
So it is really the code calling 'Access that has to worry about whether the
preconditions will be satisfied at the point of any indirect call.  That seems
about right.

> I'm presuming that in this model, the Pre'Class aspects are "or"ed
> together, then the result is "and"ed with Pre. If there is no
> Pre'Class, it is treated as True.

Yes, that is effectively what I am proposing.

>
> I'd hope that we continue to have the Pre'Class model as I laid out in
> my wording proposal (that we use the Pre'Class of the statically
> identified subprogram, which is necessarily the same or stronger than
> the Pre'Class of the invoked body). And then Pre of the invoked body would be evaluated.

Right, though I would still allow the additional Pre'Class aspects to be
*evaluated*, even if the caller isn't aware of them.

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

From: Randy Brukardt
Sent: Thursday, March 24, 2011  1:43 PM

> Cyrille from AdaCore finds the whole Pre'Class inheritance "or"-ing
> thing unpleasant, and I think there are others who might have the same
> view, and it seems potentially a benefit if Pre and Pre'Class are
> treated independently.
>
> Note that this doesn't come up for Post and Post'Class, since
> everything is and-ed together.

OK, I'll think about this in wording terms.

> > One thing that immediately comes to mind is how Pre'Class is treated
> > vis-a-vis access-to-subprogram. One of the advantages of the model
> > that I proposed is that access-to-subprogram is treated the same way
> > as a similar dispatching call (one without a Pre'Class aspect). I
> > don't see how that could work in the model you are suggesting; since
> > Pre'Class would be unknown (and thus True), it would be ignored on
> > any access-to-subprogram call (at least unless we allowed Pre'Class
> > on access-to-subprogram types). Sounds like a nasty hole.
>
> The model I thought we were talking about for access-to-subprogram was
> that you effectively created a call at the point of the 'Access, and
> whatever Pre'Class or Pre aspects that would be enforced at that point
> are the Pre'Class/Pre that would be enforced at the point of any call
> through that access value.  That seems very well defined, and yes,
> does imply a wrapper in some implementations.  So it is really the
> code calling 'Access that has to worry about whether the preconditions
> will be satisfied at the point of any indirect call.  That seems about
> right.

OK, again I'll try to think about this in wording terms.

> > I'm presuming that in this model, the Pre'Class aspects are "or"ed
> > together, then the result is "and"ed with Pre. If there is no
> > Pre'Class, it is treated as True.
>
> Yes, that is effectively what I am proposing.
> >
> > I'd hope that we continue to have the Pre'Class model as I laid out
> > in my wording proposal (that we use the Pre'Class of the statically
> > identified subprogram, which is necessarily the same or stronger
> > than the Pre'Class of the invoked body). And then Pre of the
> invoked body would be evaluated.
>
> Right, though I would still allow the additional Pre'Class aspects to
> be *evaluated*, even if the caller isn't aware of them.

Do we need wording for that? I had thought that was irrevelant (if the compiler
wants to evaluate 50 digits of PI between each statement, it is allowed to do
that). Or is there some issue with side-effects?

Anyway, you need to think about the implicit body wording that you thought was
too "mechanistic". Since that only exists to fix various problems with
Pre'Class/Post'Class/Type_Invariant'Class combinations, and nothing said above
has any effect on those problems, we still need that wording or something
equivalent. I tried to explain how I arrived at that wording in a previous
message, hopefully so that you or someone else could come up with a better idea
of how to approach it wording-wise. Please help (or decide to live with my
proposal)...

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

From: Tucker Taft
Sent: Thursday, March 24, 2011  2:57 PM

>> Right, though I would still allow the additional Pre'Class aspects to
>> be *evaluated*, even if the caller isn't aware of them.
>
> Do we need wording for that? I had thought that was irrevelant (if the
> compiler wants to evaluate 50 digits of PI between each statement, it
> is allowed to do that). Or is there some issue with side-effects?

I think the bigger issue is if one of them evaluates to True even though the one
visible to the caller evaluates to False, can we go ahead and execute the body.

> Anyway, you need to think about the implicit body wording that you
> thought was too "mechanistic". Since that only exists to fix various
> problems with Pre'Class/Post'Class/Type_Invariant'Class combinations,
> and nothing said above has any effect on those problems, we still need
> that wording or something equivalent. I tried to explain how I arrived
> at that wording in a previous message, hopefully so that you or
> someone else could come up with a better idea of how to approach it
> wording-wise. Please help (or decide to live with my proposal)...

I'll see if I can come up with something less mechanistic.

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

From: Randy Brukardt
Sent: Thursday, March 24, 2011  3:19 PM

> >> Right, though I would still allow the additional Pre'Class aspects
> >> to be *evaluated*, even if the caller isn't aware of them.
> > Do we need wording for that? I had thought that was irrevelant (if
> > the compiler wants to evaluate 50 digits of PI between each
> > statement, it is allowed to do that). Or is there some issue with side-effects?
>
> I think the bigger issue is if one of them evaluates to True even
> though the one visible to the caller evaluates to False, can we go
> ahead and execute the body.

That's not a "bigger issue"; it's the whole point of the rule. The answer is
"NO"! Because there is no way to allow that and still have a check at the call
site. (You can evaluate the preconditions you know about at the call site, but
if you can't raise an exception when they evaluate to False [because some
precondition you don't know about might be True], what is the point? The only
other way to implement that would be to pass in what you know as an additional
parameter, which seems way over the top.)

I've repeatedly said that we have to require the checking of the stronger
precondition, because it is consistent with the caller's view of the world, and
it is the only way to do the check at the call site. Moreover, I'm dubious that
"weakening" the class-wide precondition is useful in practice -- and since
"strenghtening" it violates LIS, in most programs it will be the same all the
way up. (Meaning this only will matter in corner cases.)

The only reason to worry about evaluation of the others is because you want to
generate them in the body (or wrapper) for some reason. But that does not appear
to be necessary (assuming we use my "required body" model for the messy cases).
In that case, why even allow it?

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

From: Tucker Taft
Sent: Thursday, March 24, 2011  4:28 PM

I guess what I was considering, at least for a moment, was whether we wanted it
to be "OK" for it be *unspecified* whether an exception is raised in the case
where the weaker Pre'Class is satisfied but the caller-visible Pre'Class is
*not* satisfied.

I admit that sounds pretty weird...  And it sure sounds like bad news for
portability.

So I guess I am convinced that you *must* do Pre'Class checks at the call site,
and only at the call site.

I do think this begins to argue pretty strongly for separating out "Pre" from
Pre'Class, and effectively putting the "Pre" checks in the body (though *not*
handleable! -- they are like a pragma Assert in the outer declarative part of
the subprogram), along with the Post and Post'Class, while the Pre'Class checks
remain strictly at the caller, and are based on the particular "view" denoted by
the caller, not by the body actually reached.

I also think that for access-to-subprogram, if the designated subprogram has a
Pre'Class aspect, the access value generated by 'Access must designate a wrapper
that checks it (unless of course Assertions are being ignored).  Otherwise, a
simple way of bypassing a Pre'Class check would be to declare a local
access-to-subprogram type, and then call through that.  Hardly seems desirable.

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

From: Randy Brukardt
Sent: Thursday, March 24, 2011  3:32 PM

...
> The current rules proposal does not allow any Pre/Post exceptions to
> be handled by the body, and I think that is exactly right. Your
> assertion that we never discussed it is wrong; we discussed it
> ad-nausem at the Tallehasse meeting (I think you missed that one,
> probably why you don't know that).
> 13.3.2(18/3) is pretty clear that this is the intent. The reason is
> that for statically bound cases, we ought to let the compiler have the
> freedom to generate the checks wherever it wants (in the body or at
> the call site) - in order to maximize the possibilities for
> optimization/proof.
> Dispatching calls and access-to-subprogram are different, of course.

One additional point I thought of on the way home last night: the body of a
subprogram does not necessarily know about all of the postconditions that apply
to it. Additional ones can be added to inherited versions via progenitors. Those
also have to be evaluated, and I can't think of any sane way to do that so that
the exception could be handled within the body. (You could pass in a thunk with
such postconditions, but that would be a lot of overhead for something that is
going to happen very rarely.) The other possibility would be to make such
subprograms illegal in some way (one of the options I already considered for
this case); but that requires users to write wrappers by hand, with all of the
possibilities for error that entails.

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

From: Tucker Taft
Sent: Thursday, March 24, 2011  4:14 PM

I agree we discussed the issue of handling pre/post-condition exceptions and
concluded they should *not* be handle-able in the body. Let's not re-open that
one.

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

From: Robert Dewar
Sent: Thursday, March 24, 2011  6:03 PM

> One additional point I thought of on the way home last night: the body
> of a subprogram does not necessarily know about all of the
> postconditions that apply to it. Additional ones can be added to
> inherited versions via progenitors. Those also have to be evaluated,
> and I can't think of any sane way to do that so that the exception
> could be handled within the body. (You could pass in a thunk with such
> postconditions, but that would be a lot of overhead for something that
> is going to happen very rarely.) The other possibility would be to
> make such subprograms illegal in some way (one of the options I
> already considered for this case); but that requires users to write
> wrappers by hand, with all of the possibilities for error that entails.

If true, this is very worrisome, I don't see any easy way for us to accomodate
that in our implementation

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

From: Randy Brukardt
Sent: Thursday, March 24, 2011  7:11 PM

The model that Tucker and I have been discussing is that for such inherited
subprograms, the semantics is as if there was an explicit body for the routine
(complete with the expected postcondition checks, if you are doing them inside
of the body), which just calls the parent routine. This seems to be about as
hard to implement as the other cases where you have to generate a wrapper for a
tag or a use of 'Access, so I don't think there can be a major implementation
problem. If there is, however, we probably should use the "requires overriding"
solution instead (which would insist that the client write an explicit body for
the routine).

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

From: Tucker Taft
Sent: Thursday, March 24, 2011  7:44 PM

> If true, this is very worrisome, I don't see any easy way for us to
> accomodate that in our implementation

Randy was simply giving more reasons why exceptions arising from postconditions
shouldn't be handleable in the body.  But we decided a long time ago that these
exceptions are not handle-able inside the body, so this whole thread is merely
reinforcing that decision.

Actually adding the additional postcondition checks isn't that hard, it just
means creating a wrapper.  But Randy's point was that such a wrapper cannot
raise an exception that could be handled inside the body it is wrapping!  But
who cares, since we don't want the exception to be handle-able anyway.

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

From: Tucker Taft
Sent: Thursday, March 24, 2011  5:24 PM

> I also think that for access-to-subprogram, if the designated
> subprogram has a Pre'Class aspect, the access value generated by
> 'Access must designate a wrapper that checks it (unless of course
> Assertions are being ignored). Otherwise, a simple way of bypassing a
> Pre'Class check would be to declare a local access-to-subprogram type,
> and then call through that. Hardly seems desirable.

Alternatively, we say that a subprogram to which a Pre'Class aspect applies has
effectively an "Intrinsic" convention, so you can't take 'Access of it.  That
would mean the compiler wouldn't have to create the wrapper.  The user could of
course always create an explicit wrapper if they needed one.

OK, this brings up another Baird-ish question:  What happens if you rename a
subprogram to which a Pre'Class applies. Does it still apply?  If you rename it
to be something that is not a dispatching operation, then it is only interesting
if it is non-abstract, and you can only call it in a non-dispatching way, so it
feels like it should still be subject to the same Pre'Class check.  But we have
a rule that you can't specify a Pre'Class attribute on anything but a
dispatching operation.  But we aren't really specifying it, we are just carrying
it over.  It would again seem weird if you could get rid of the effect of a
Pre'Class aspect simply by renaming the subprogram. Perhaps we are adopting the
renaming-as-body semantics, which is essentially a wrapper model.

OK, now here is the killer follow-up:  What happens if you rename it to be
another dispatching operation, and it overrides an inherited subprogram which
had its own Pre'Class attribute? This feels like trouble, and almost argues for
the same trick suggested above for access-to-subprogram, namely disallow the
rename, since effectively the "conventions" don't match, where "convention" has
now been augmented to include the Pre'Class aspect, since that certainly affects
what you have to do at the call site.

The simplest solution to all of these problems might be to say that subtype
conformance (which is needed for 'Access, overriding, and renaming-as-body)
requires that the "same" Pre'Class aspects, if any, apply to both subprograms
(for overriding, clearly this has to allow a new Pre'Class aspect to be applied
*after* the overriding occurs -- which is sort of OK, since aspect specs don't
get elaborated until the freezing point).

This also implies that if some day we allow Pre'Class aspects on access-to-subp,
then that might be a way to support 'Access on these guys (though it doesn't
seem like an important capability at this point).

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

From: Randy Brukardt
Sent: Thursday, March 24, 2011  7:21 PM

Fascinating. I proposed something like this a while back, but rejected it as too
outlandish. I personally would go further and *not* allow further specification
of Pre'Class (or Post'Class or Type_Invariant'Class for that matter). Then there
is no combination cases, no one is confused by "or" or "and". We don't need
implicit bodies when there is multiple inheritance. If you need to add some
precondition, you still have Pre/Post/Type_Invariant.

This indeed is my model of how these should work -- modifying Pre'Class or
Post'Class on a dispatching routines just does not make sense to me -- we don't
allow that for any other property. And I cannot think of any significant reason
why you would want to do this in practice. (Maybe there is some reason relating
to multiple inheritance -- I don't think too hard about that.)

But I thought all of this would end up way too limiting. Especially because
there isn't any way for it to allow no precondition to match, making it much
harder to match interfaces. And I can't see any way to add Pre'Class to subtype
conformance and then somehow not have it apply to an overriding routine. That
would be a major change in model -- it would invalidate 3.9.2(10/2) which seems
to be the cornerstone of Ada OOP. (At least of the implementability of Ada OOP.)

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

From: Tucker Taft
Sent: Thursday, March 24, 2011  7:59 PM

> Fascinating. I proposed something like this a while back, but rejected
> it as too outlandish. I personally would go further and *not* allow
> further specification of Pre'Class (or Post'Class or
> Type_Invariant'Class for that matter). Then there is no combination
> cases, no one is confused by "or" or "and". We don't need implicit
> bodies when there is multiple inheritance. If you need to add some precondition, you still have Pre/Post/Type_Invariant.

I am *not* recommending that.  You can still override, but you can't do so by
renaming another dispatching operation that already has a Pre'Class. And you
*can* weaken the Pre'Class if you wish.

I think that is important because the Pre'Class on the root type might be too
strong for some important subtree of the type hierarchy. That subtree should be
able to have a weaker Pre'Class if it makes sense in that subtree.

> This indeed is my model of how these should work -- modifying
> Pre'Class or Post'Class on a dispatching routines just does not make
> sense to me -- we don't allow that for any other property.

I don't follow you when you say "any other property."  To what are you
referring.  Clearly the 'Address, the names of the formal parameters, the
default expressions, whether the routine is inlined, and most importantly the
code itself, can change with the overriding.

> ... And I cannot think of any
> significant reason why you would want to do this in practice. (Maybe
> there is some reason relating to multiple inheritance -- I don't think
> too hard about that.)

I don't agree; weakening the Pre'Class can make sense as you go into a
particular subtree of the type hierarchy.

> But I thought all of this would end up way too limiting. Especially
> because there isn't any way for it to allow no precondition to match,
> making it much harder to match interfaces.

I believe you are going to far.  I was using the subtype conformance as a way to
eliminate various unpleasant cases that require wrappers. I am not suggesting we
break the whole model, just that we effectively outlaw things like 'Access and
weird renamings.

> ... And I can't see any way to add Pre'Class to subtype conformance
> and then somehow not have it apply to an overriding routine.

This just requires a wording tweak in my view.  Para 3.9.2(10/2) now says:

    ... If the dispatching operation overrides an inherited
    subprogram, it shall be subtype conformant with the inherited
    subprogram. ...

If we add Pre'Class matching to subtype conformance, then that is almost exactly
what we want.  But after the overriding takes place, we want to allow further
weakening of the Pre'Class, so if necessary we add something to the above
sentence to make it clear that that is OK.

> ... That would be a major change in model -- it would invalidate
> 3.9.2(10/2) which seems to be the cornerstone of Ada OOP. (At least of
> the implementability of Ada OOP.)

I'm not suggesting we drop the above sentence, but rather have it say something
about Pre'Class if necessary to allow weakening it, but not replacing the
Pre'Class via a renaming of some other dispatching operation which has a
completely different Pre'Class.

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

From: Randy Brukardt
Sent: Thursday, March 24, 2011  8:31 PM

> I don't follow you when you say "any other property."  To what are you
> referring.  Clearly the 'Address, the names of the formal parameters,
> the default expressions, whether the routine is inlined, and most
> importantly the code itself, can change with the overriding.

"Interesting" property visible in the contract: constraints, no-return, not
null, predicates, "Is_Synchronized", etc.

My personal feeling is that allowing the parameter names and defaults to change
was a mistake, but not a very important one.

> > ... And I cannot think of any
> > significant reason why you would want to do this in practice. (Maybe
> > there is some reason relating to multiple inheritance -- I don't
> > think too hard about that.)
>
> I don't agree; weakening the Pre'Class can make sense as you go into a
> particular subtree of the type hierarchy.

I would like to see an example of why you would want this in practice (not in
theory!!). There is a lot of OOP stuff that makes sense in theory but never
actually happens in practice. Needing to "weaken" the precondition seems to me
like there was a bug in the original definition of the precondition (most
likely, the boolean functions that make it up are not defined properly). But I
am willing to believe that I am wrong -- but to do that I'd need to see an
example for which the weaker precondition makes sense.

> > But I thought all of this would end up way too limiting. Especially
> > because there isn't any way for it to allow no precondition to
> > match, making it much harder to match interfaces.
>
> I believe you are going to far.  I was using the subtype conformance
> as a way to eliminate various unpleasant cases that require wrappers.
> I am not suggesting we break the whole model, just that we effectively
> outlaw things like 'Access and weird renamings.

Fine, but then you can't do it with subtype conformance, since overriding
routines are required to be subtype conformant.

> > ... And I can't see any way to add Pre'Class to subtype conformance
> > and then somehow not have it apply to an overriding routine.
>
> This just requires a wording tweak in my view.  Para
> 3.9.2(10/2) now says:
>
>     ... If the dispatching operation overrides an inherited
>     subprogram, it shall be subtype conformant with the inherited
>     subprogram. ...
>
> If we add Pre'Class matching to subtype conformance, then that is
> almost exactly what we want.  But after the overriding takes place, we
> want to allow further weakening of the Pre'Class, so if necessary we
> add something to the above sentence to make it clear that that is OK.

Then you're breaking the definition of subtype conformance. That seems really
bad to me; in large part because it seems likely that you'll want other such
exceptions in the future. It just turns into a morass.

> > ... That would be a major change in model -- it would invalidate
> > 3.9.2(10/2) which seems to be the cornerstone of Ada OOP. (At least
> > of the implementability of Ada OOP.)
>
> I'm not suggesting we drop the above sentence, but rather have it say
> something about Pre'Class if necessary to allow weakening it, but not
> replacing the Pre'Class via a renaming of some other dispatching
> operation which has a completely different Pre'Class.

That just does not make any sense. You're saying that it has to be subtype
conformant, but it is OK for it not to be subtype conformant sometimes. That way
lies madness (mine :-).

I do agree that requiring that always it too strong a restriction, so I think
you have to change something else. Perhaps we need a fifth kind of conformance
(subtype - Pre'Class) -- "overriding conformance" which is the current
definition of subtype conformance. Then add "subtype conformance" which would be
the current kind + Pre'Class??

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

From: Bob Duff
Sent: Thursday, March 24, 2011  7:24 PM

> If true, this is very worrisome, I don't see any easy way for us to
> accomodate that in our implementation

Is there any hope that I can get through this email thread without reading all
of it?  Randy and Tuck have been going at it for 3 days, and I've saved the
emails unread. Do I need to read all the emails?

I think it's important and I need to understand the issues, but I feel
overwhelmed.  Any possibility of a summary?

P.S. I think we should at least ALLOW preconditions to be checked at the call
site.

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

From: Tucker Taft
Sent: Thursday, March 24, 2011  8:13 PM

Here is what we are debating:

    1) Must Pre'Class be checked at the call site,
       or could it be done inside the body?
        Answer: we seem to agree it only makes sense
          if it is done at the point of call, and only
          the Pre'Class aspects known at the point of call
          are checked.

    2) Should specifying a Pre'Class have any affect on
       the "Pre" aspects?
         Tuck's Answer: No, let's split them completely.
            This allows (and pretty much requires) "Pre" aspects
            to be checked in the body.
         Randy's Answer: Not sure.

    3) What are some of the implications of renaming and taking
        'Access of a subprogram to which Pre'Class applies?
           Tuck's Answer: Make hard stuff illegal, by incorporating
             Pre'Class matching into subtype conformance, but still
             allow Pre'Class weakening.
           Randy's Answer: Not sure.  Maybe disallow Pre'Class weakening
             completely.

One other issue that seems clear is that when you inherit code for an operation
from a parent type, and you also inherit the "same" operation from one or more
interfaces where the operation has a Post'Class aspect, you will probably have
to create a wrapper to properly incorporate the inherited Post'Class aspects
into the inherited code, since they all get and-ed together.

Randy can fill in more if I have forgotten something.

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

From: Randy Brukardt
Sent: Thursday, March 24, 2011  8:43 PM

>     2) Should specifying a Pre'Class have any affect on
>        the "Pre" aspects?
>          Tuck's Answer: No, let's split them completely.
>             This allows (and pretty much requires) "Pre" aspects
>             to be checked in the body.
>          Randy's Answer: Not sure.

I think you've convinced me on this one.

>     3) What are some of the implications of renaming and taking
>         'Access of a subprogram to which Pre'Class applies?
>            Tuck's Answer: Make hard stuff illegal, by incorporating
>              Pre'Class matching into subtype conformance, but still
>              allow Pre'Class weakening.
>            Randy's Answer: Not sure.  Maybe disallow Pre'Class weakening
>              completely.

I'm not against the idea, I'm against the execution. I'm surely in favor of
making hard stuff illegal!

> One other issue that seems clear is that when you inherit code for an
> operation from a parent type, and you also inherit the "same"
> operation from one or more interfaces where the operation has a
> Post'Class aspect, you will probably have to create a wrapper to
> properly incorporate the inherited Post'Class aspects into the
> inherited code, since they all get and-ed together.

This also applies to Type_Invariant'Class (it works like Post'Class in that
sense).

This latter issue is the "bug"; this has to be addressed or we will have
problems with missed Pre'Class/Post'Class in inherited operations (bodies that
get called without their preconditions being satisfied are really bad. The other
things are all about making the model better, we could live without them but
everyone will be happier if we don't.

> Randy can fill in more if I have forgotten something.

I think that is it. Lots of examples in my various e-mails; it will help to go
back and make sure those all make sense in the end.

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

From: Randy Brukardt
Sent: Friday, March 25, 2011  10:53 PM

I've been trying to work on the wording for this AI, and...

...
> The simplest solution to all of these problems might be to say that
> subtype conformance (which is needed for 'Access, overriding, and
> renaming-as-body) requires that the "same"
> Pre'Class aspects, if any, apply to both subprograms (for overriding,
> clearly this has to allow a new Pre'Class aspect to be applied *after*
> the overriding occurs -- which is sort of OK, since aspect specs don't
> get elaborated until the freezing point).

I don't understand why you only are worrying about renames-as-body here. Doesn't
renames-as-declaration have the same problem? An overriding is not a completion,
after all, it is a new declaration of a homograph.

The problem in question is renaming a routine that has one or more class-wide
preconditions as an overriding of another routine that has one or more different
class-wide preconditions. We can only allow weakening, but this is not likely to
be that. I don't see any reason that you can't use a renames-as-declaration in
such a context.

("Class-wide preconditions" is the nice name I gave Pre'Class in my wording
proposal - trying to talk about Pre'Class separately from Pre is beyond what I
can do wording-wise.)

If that's the case, modifying subtype conformance does not do the trick, since
renames-as-declaration only needs mode-conformance. We probably need separate
legality rules in that case.

The basic problem (both for renames and for access-to-subprogram) is that we
don't allow specifying the class-wide precondition, so we have to assume "True"
and that starts to get weird.

===============

The aspects of a renames are the same as the renamed entity (unless otherwise
specified), so there does not seem to be a problem with any sort of renames that
isn't overriding. So I have to think we just want a hack to cover that case.

Indeed, all we really need to do is declare that a renames is just a shorthand
for an explicit body in this case; indeed this is exactly the same sort of
problem that occurs via multiple inheritance. We should solve these the same way
(either make both illegal, with a specific rule) or just use the rules I've
previously laid out.

The access-to-subprogram also might as well get a specific Legality Rule.

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

From: Randy Brukardt
Sent: Friday, March 25, 2011  11:59 PM

Attached find a new draft of the AI (version /03) covering these issues. I fear
that I didn't do a very good job of explaining the overall model, but I was
concentrating on the wording changes needed. Now back to pragmas => aspects.

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