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
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Quick question regarding limited type return syntax
Date: Mon, 04 Aug 2014 18:19:16 +0200
Organization: A noiseless patient Spider
Message-ID: <lrobq5$kvj$1@dont-email.me>
References: <166aaec5-5e9c-40e0-9b07-9b9c7d5f7f33@googlegroups.com>
 <EngCv.101926$Ji3.44609@fx16.iad>
 <16a6846f-2964-438a-ab9b-2029075f7924@googlegroups.com>
 <bf9193d6-e1a8-4df3-8e36-b07a2b07655e@googlegroups.com>
 <lret2q$fs$1@loke.gir.dk> <lrfh8k$rpi$1@dont-email.me>
 <lrgpg1$40g$1@loke.gir.dk> <D7TCv.160339$HF6.16263@fx30.iad>
 <c43h9sFgdq8U1@mid.individual.net>
 <20m59uxjlygw$.2mpabkt469vp.dlg@40tude.net>
 <wcciombyqmq.fsf@shell01.TheWorld.com>
 <cp8rrf40gpmj.zx1py68uwkjl$.dlg@40tude.net>
 <wccegwzyn76.fsf@shell01.TheWorld.com>
 <a5pzvn575hsz.8rt38rwse8bg.dlg@40tude.net> <c450cgFq3u2U1@mid.individual.net>
 <vuqtsin4324j$.1qqhcwhbgnd21.dlg@40tude.net>
 <c491psFkt2bU1@mid.individual.net>
 <1ge2ly0v5yk8d.j8pd98xg0o8v.dlg@40tude.net>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 4 Aug 2014 16:19:17 +0000 (UTC)
Injection-Info: mx05.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="21491"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/1cAsa7f7In2epbE6rRXO5/bfiVg1SwWE="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:24.0) Gecko/20100101 Thunderbird/24.6.0
In-Reply-To: <1ge2ly0v5yk8d.j8pd98xg0o8v.dlg@40tude.net>
Cancel-Lock: sha1:1Pi32rI46cus+rwbTg0/wo5SI7Q=
Xref: news.eternal-september.org comp.lang.ada:21444
Date: 2014-08-04T18:19:16+02:00
List-Id: <comp.lang.ada>

On 04.08.14 14:43, Dmitry A. Kazakov wrote:

> To make it clearer consider what would be the post-condition of Initialize:
>
>     type T is ...;
>     type S is new T ...;
>
>     Initialize (X : in out T)
>        ensure
>           T'Operational (X)
>
> [*] or, maybe
>
>           S'Operational (X)
>           T'Class'Operational (X)
>           S'Class'Operational (X)
>
> Now, the precondition of a dispatching call on T'Class is obviously:
>
>     require
>        T'Class'Is_Operational (X)

The model is circular, I think, in that you stipulate
that 'Operational must be a "premiss" for a dispatching call,
using "obvious" as the sole reason. But while I think that
everything else is a hack, some specific dispatching scenario
need not even require the allocation of any of the derived
type's components, for when no callee needs them, they don't
matter, and still the whole object is 'Operational (in this
sense).

Not that I can now think of a case that is both useful and
cannot be "architected" in some other, perhaps better way.