Re: Class wide preconditions: error in GNAT implementation?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Mon, 18 Feb 2013 09:17:57 +0000, Simon Wright wrote:

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

LSP is wrong in general. A narrower "truer" version of LSP applies
specifically to operations and their preconditions and all that in the
context of substitutability, which is not the case for a dispatching call.
A dispatching call does not substitute unless the body is inherited.

Anyway, trivially, consider the following types:

   type A is ...;
   type B is new A with ...;

The predicate P=x in A'Class is true for both A and B. The predicate Q=y in
B'Class is true B and false for A. hence Q=>P, Q is stronger.

[Tag checks violate LSP]

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

Yes, but the major crime here is mingling correctness with program
semantics. The thing meant to be executed in the prologue of an operation
has nothing to do with correctness, it is about operation composition upon
inheritance and/or about object construction.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de