From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,df055ffdd469757d
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.68.210.15 with SMTP id mq15mr1757782pbc.2.1361848968090;
        Mon, 25 Feb 2013 19:22:48 -0800 (PST)
Path: 
 ov8ni20804pbb.1!nntp.google.com!border1.nntp.dca.giganews.com!border1.nntp.ams.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!news.teledata-fn.de!weretis.net!feeder4.news.weretis.net!eternal-september.org!feeder.eternal-september.org!mx05.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: Class wide preconditions: error in GNAT implementation?
Date: Mon, 18 Feb 2013 20:42:56 +0000
Organization: A noiseless patient Spider
Message-ID: <lyppzxpd4f.fsf@pushface.org>
References: <e155e2d6-ba1f-4fc0-a6e3-dafde002670b@googlegroups.com>
	<kfmlq1$puv$1@munin.nbi.dk>
	<30edd381-7505-496a-99e5-f884faf33c33@googlegroups.com>
	<16s3mt7cm3n61$.8qu6fp1nglfq.dlg@40tude.net>
	<bf5a32d8-6ee9-413d-83ed-c2f076e065e4@googlegroups.com>
	<1a648dqoysnp4$.7l9zsp043d2e.dlg@40tude.net>
	<377a4b9b-eec8-4af9-af3f-fdeb008339e4@googlegroups.com>
	<1hjhzbhx5ryn7$.rst5open618c.dlg@40tude.net>
	<ly621qq8u2.fsf@pushface.org>
	<1r2tvdtl13at0.3nopie8tus4v.dlg@40tude.net>
	<lytxp9pkfu.fsf@pushface.org>
	<1d2fr74npgdwt$.mcfs4zhtbvg6$.dlg@40tude.net>
Mime-Version: 1.0
Injection-Info: mx05.eternal-september.org;
 posting-host="4b4553eac4247089c1d7c0bcc27eb5e3";
	logging-data="22082"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX183NIztnHkTsB9WnABwf1/4PjJVNiZd0YE="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.2 (darwin)
Cancel-Lock: sha1:q/4zrr+YThKifBh/Lz7jiHUCjA0=
	sha1:DkiUfmZ1uvyGNkF1qSpjITH0Nsk=
Content-Type: text/plain
Date: 2013-02-18T20:42:56+00:00
List-Id: <comp.lang.ada>

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