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.180.98.103 with SMTP id eh7mr2383915wib.3.1361849315870;
        Mon, 25 Feb 2013 19:28:35 -0800 (PST)
Path: 
 bp2ni59445wib.1!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.131.MISMATCH!xlned.com!feeder3.xlned.com!newsfeed.xs4all.nl!newsfeed3.news.xs4all.nl!xs4all!usenetcore.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!feeder1.news.weretis.net!news.swapon.de!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 18:04:53 +0000
Organization: A noiseless patient Spider
Message-ID: <lytxp9pkfu.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>
Mime-Version: 1.0
Injection-Info: mx05.eternal-september.org;
 posting-host="4b4553eac4247089c1d7c0bcc27eb5e3";
	logging-data="29898"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19ouxlB3D1VYwT7MI+V4WkeF3VduO6D0kc="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.2 (darwin)
Cancel-Lock: sha1:Q47jRb0Qz3VPILeRK8lqej6ae2E=
	sha1:6WUIYCJoUMShaOqb3IkrgutbZ2E=
Content-Type: text/plain
Date: 2013-02-18T18:04:53+00:00
List-Id: <comp.lang.ada>

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

> 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? No problem if you
don't have any class-wide calls, but you've just eliminated dispatching.

> [Tag checks violate LSP]

Don't understand.

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