Re: Class wide preconditions: error in GNAT implementation?

[ytomino <aghia05@gmail.com>]

On Sunday, February 17, 2013 1:35:12 AM UTC+9, Dmitry A. Kazakov wrote:
> On Sat, 16 Feb 2013 05:13:53 -0800 (PST), ytomino wrote:
> >>> In this case, the caller should keep As.foo'Pre'Class because calling As.foo.
> >> No, the caller shall satisfy the precondition of the callee. Regarding
> >> inheritance, a primitive operation (callee) may weaken the precondition it
> >> overrides. This is why logical disjunction apply, as Randy said.
> > No. The caller is "client" of not Bs but As, in this case.
> 
> The precondition of a dispatching call is one of the class. The
> precondition of the specific operation can be weaker. The precondition of a
> LSP subclass can be stronger. All three shall be satisfied by the caller,
> but only the first one is actually constraining for it, because the second
> two are automatically satisfied through the mechanism of dispatching call
> and type coercion.

Yes. *only the first one* = only As.foo'Pre'Class should be satisfied.

> >> Considering individual terms of the disjunction, the caller is allowed to
> >> satisfy at least one of them to make the call valid.
> > Imagine, the system is running correctly, but depending on weak precondition of the subclass.
> > On day, new subclass is introduced into this system.
> > This new subclass has strong precondition equally to the superclass.
> > But, existing callers is depending on weak one.
> > It's a bug of callers, not subclasses.
> 
> It won't happen. A weakened precondition apply to the another caller, an
> imaginary polymorphic body which is called by the original caller. When you
> arrive into that body and go trough the tag-case, and are ready to call the
> specific body, then the precondition of the latter apply. Original caller
> has to satisfy the precondition of the operation it calls. For a
> dispatching operation it is one of the class.

Are you imagining the dispatcher like below?

procedure foo_Dispatcher (Object : A'Class) is
begin
   pragma Assert (As.foo'Pre'Class);
   case Object'Tag is
      when A'Tag =>
         As.foo (A (Object));
      when B'Tag =>
         pragma Assert (Bs.foo'Pre'Class); -- unnecessary because weaker
         Bs.foo (B (Object));
      ...
   end case;
end foo_Dispatcher;

If it is, your understanding is same as mine.

I'll repeat what I said. I believe the specification in Ada RM(AARM) is right
and merely point out the error in the behavior of GNAT.
The behavior of GNAT is different from what you says.