Re: Quick question regarding limited type return syntax

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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