Re: Class wide preconditions: error in GNAT implementation?

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

On Mon, 18 Feb 2013 20:42:56 +0000, Simon Wright wrote:

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

But that is not same as correctness. Even if substitutability were
decidable that would not ensure correctness. And conversely a program can
be correct even with substitutability violated.

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

The first is trivial, the second is undecidable.

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

But the idea of LSP (behavioral notion of subtype) was to prevent such
predicates coming into existence per construction of subtypes. The sad
reality is that we need them to make our programs working, e.g. for
dispatching. Mere existence of predicates which do not hold upon subtyping
does not make program incorrect and sometimes they do it correct.

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