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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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.102 with SMTP id eh6mr2387012wib.7.1361849738997; Mon, 25 Feb 2013 19:35:38 -0800 (PST) Path: g1ni33279wig.0!nntp.google.com!feeder1.cambriumusenet.nl!194.109.133.87.MISMATCH!newsfeed.xs4all.nl!newsfeed1.news.xs4all.nl!xs4all!feeder3.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.cambriumusenet.nl!feed.tweaknews.nl!216.196.110.146.MISMATCH!border3.nntp.ams.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!rt.uk.eu.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Class wide preconditions: error in GNAT implementation? Date: Tue, 19 Feb 2013 10:07:28 +0100 Organization: cbb software GmbH Message-ID: <11ib1znk4xdxd$.a0hnpfw4er6b$.dlg@40tude.net> References: <30edd381-7505-496a-99e5-f884faf33c33@googlegroups.com> <16s3mt7cm3n61$.8qu6fp1nglfq.dlg@40tude.net> <1a648dqoysnp4$.7l9zsp043d2e.dlg@40tude.net> <377a4b9b-eec8-4af9-af3f-fdeb008339e4@googlegroups.com> <1hjhzbhx5ryn7$.rst5open618c.dlg@40tude.net> <1r2tvdtl13at0.3nopie8tus4v.dlg@40tude.net> <1d2fr74npgdwt$.mcfs4zhtbvg6$.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2013-02-19T10:07:28+01:00 List-Id: On Mon, 18 Feb 2013 20:42:56 +0000, Simon Wright wrote: > "Dmitry A. Kazakov" writes: > >> On Mon, 18 Feb 2013 18:04:53 +0000, Simon Wright wrote: >> >>> "Dmitry A. Kazakov" 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