Re: Class wide preconditions: error in GNAT implementation?

[Simon Wright <simon@pushface.org>]

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

> On Mon, 18 Feb 2013 18:04:53 +0000, Simon Wright wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>> 

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

Well, you've consructed a situation which is plainly wrong if we're
going to be talking substitutablity.

I would expect that if you could prove that

  * all calls via A'Class meet A's precondition; and

  * all derived type implementations produce valid output when given
    parameters that meet A's precondition

then you'd be a long way toward a correctness proof.

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

Then don't write predicates like that! (and slap the wrist of anyone you
find doing it).