Re: Quick question regarding limited type return syntax

["G.B." <bauhaus@futureapps.invalid>]

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.