Re: Class wide preconditions: error in GNAT implementation?

[Simon Wright <simon@pushface.org>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Sat, 16 Feb 2013 11:55:55 -0800 (PST), ytomino wrote:
>
>> 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.
>
> No, all preconditions must be satisfied, otherwise, the program is
> incorrect, provided it is correctness we are talking about.
[...]
> But then the precondition of B'Class is *required* to be true for an
> object which is in that class. The precondition of A'Class is weaker
> and need not to be checked if one for B'Class is satisfied.

This is the wrong way round. A subclass can only _weaken_ the
precondition of the superclass. Anything else violates LSP.

This new feature introduces a whole new opportunity for error: getting
the preconditions wrong.