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.76.235 with SMTP id n11mr2383931wiw.0.1361849511920;
        Mon, 25 Feb 2013 19:31:51 -0800 (PST)
Path: 
 bp2ni59449wib.1!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.103.MISMATCH!feeder3.cambriumusenet.nl!feed.tweaknews.nl!216.196.110.142.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!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 09:17:57 +0000
Organization: A noiseless patient Spider
Message-ID: <ly621qq8u2.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>
Mime-Version: 1.0
Injection-Info: mx05.eternal-september.org;
 posting-host="4b4553eac4247089c1d7c0bcc27eb5e3";
	logging-data="23372"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18xw+lAdZYEzvEiQi1IeLrTxa9iCA4+THY="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.2 (darwin)
Cancel-Lock: sha1:DyTq+As/cK4VD0lkoO8a9snPf90=
	sha1:nbl4WY6XGYYS46PrB269VTwLH34=
Content-Type: text/plain
Date: 2013-02-18T09:17:57+00:00
List-Id: <comp.lang.ada>

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

> On Sat, 16 Feb 2013 11:55:55 -0800 (PST), ytomino wrote:
>
>> On Sunday, February 17, 2013 1:35:12 AM UTC+9, Dmitry A. Kazakov wrote:
>>> On Sat, 16 Feb 2013 05:13:53 -0800 (PST), ytomino wrote:
>>>>>> In this case, the caller should keep As.foo'Pre'Class because
>>>>> calling As.foo.
>>>>> No, the caller shall satisfy the precondition of the
>>>>> callee. Regarding inheritance, a primitive operation (callee) may
>>>>> weaken the precondition it overrides. This is why logical
>>>>> disjunction apply, as Randy said.
>>>> No. The caller is "client" of not Bs but As, in this case.
>>> 
>>> The precondition of a dispatching call is one of the class. The
>>> precondition of the specific operation can be weaker. The
>>> precondition of a LSP subclass can be stronger. All three shall be
>>> satisfied by the caller, but only the first one is actually
>>> constraining for it, because the second two are automatically
>>> satisfied through the mechanism of dispatching call and type
>>> coercion.
>> 
>> Yes. *only the first one* = only As.foo'Pre'Class should be satisfied.
>
> No, all preconditions must be satisfied, otherwise, the program is
> incorrect, provided it is correctness we are talking about.
[...]
> 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.

This new feature introduces a whole new opportunity for error: getting
the preconditions wrong.