Re: Class wide preconditions: error in GNAT implementation?

[ytomino <aghia05@gmail.com>]

We are already inured to polymorphism. So this fact counters to our intuition.
I had been confused when I knew it. After all, I took a Eiffel book out.

On Saturday, February 16, 2013 6:28:10 PM UTC+9, Dmitry A. Kazakov wrote:
> On Fri, 15 Feb 2013 18:50:36 -0800 (PST), ytomino wrote:
> > No. It's related to correctness.
> Not when checked dynamically by the same program.
> > Precondition is a promise for caller, not callee.
> Actually it is imposed on both.

No. Precondition is imposed on only caller.

> > 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.

> 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.

"Client" code of superclass should have been fully keeping precondition of superclass all along.

In "Design by Contact", the caller of superclass has a contract with only superclass.
Randy wrote "to allow analysis without knowing the actual tag".
This word is applied to not only analyzer machine but also human programmers.

> Note that if the callee were a class-wide operation then its precondition
> would read literally.

Of course.

If you had time, please read the discussion in http://d.puremagic.com/issues/show_bug.cgi?id=6857 .
Maybe it's more easy to understand than my words.