Re: Class wide preconditions: error in GNAT implementation?

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

On Mon, 18 Feb 2013 18:04:53 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 18 Feb 2013 09:17:57 +0000, Simon Wright wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>>> 
>>>> 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.
> 
> Is there a Kazakov Substitution Principle, then? (or someone else's ...)

You can find it all around Ada. E.g. constants, in-parameters, subtypes are
examples of subtypes violating LSP.

Ada's substitutability principle is that anything is substitutable that is
not rejected by the compiler. (:-))

Liskov's motivation was to coin subtyping in terms of substitutability.
This is impossible to do without limiting the context of substitution. A
type system cannot be based on LSP, unfortunately.

>> 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.
> 
> If you allow code like this, how can you draw any conclusions about the
> correctness of a call through a pointer to A'Class?

Do you believe in correctness proofs without looking into the bodies?

>> [Tag checks violate LSP]
> 
> Don't understand.

Because these could be used to construct predicates which would depend on
the actual type. Absolute substitutability as required by "naive"
interpretations of LSP is based on types being absolutely indistinguishable
for the clients, which tags obviously defeat.

>>> 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.
> 
> The intention is (AIUI) to be able to extract {pre,post}conditions from
> an Ada program and do static verification; how is what Ada2012 does
> (dynamically) incompatible with that?

Per observation that static /= dynamic.

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