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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Quick question regarding limited type return syntax Date: Mon, 4 Aug 2014 18:38:53 +0200 Organization: cbb software GmbH Message-ID: References: <166aaec5-5e9c-40e0-9b07-9b9c7d5f7f33@googlegroups.com> <16a6846f-2964-438a-ab9b-2029075f7924@googlegroups.com> <20m59uxjlygw$.2mpabkt469vp.dlg@40tude.net> <1ge2ly0v5yk8d.j8pd98xg0o8v.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: 20F0+KuiXJUq19ljFVPmRg.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:21445 Date: 2014-08-04T18:38:53+02:00 List-Id: On Mon, 04 Aug 2014 18:19:16 +0200, G.B. wrote: > 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. How isn't obvious and how is it circular? A dispatching = primitive operation is defined on the whole class. That is the definition of. The argument of a dispatching call is of the type T'Class. This is also per definition. How can you call an operation of the type on an object of this type when the former is not yet operational? > 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). Maybe, but this does not follow from the types at hand. If the language allowed partial classes you could be able to express something like T'Class \ S -- All types derived from T but S a dispatching call to anything but Foo of S might work. That would require definition of a primitive operation of a partial class. procedure Foo (X : in out T \ S); -- Whatever -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de