Re: Quick question regarding limited type return syntax

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

On Mon, 04 Aug 2014 12:24:19 +0300, Niklas Holsti wrote:

> Controlled types in Ada provide hooks (Initialize/Finalize/Adjust) that
> can be used as constructors and destructors,

Not really. The problem is that they hook too late to be specific type
constructor and too early for a specific type destructor. This is why you
can dispatch from there. The problem arise when you attempt both: use
Initialize as if it were a specific constructor hook and dispatch from it.

> I don't agree that dispatching on a controlled object should be illegal
> until the Initialize operation on that object has been completed.

Then you cannot call Initialize a constructor's hook. These two are
mutually exclusive. You can dispatch not before all specific descendants
are constructed and T'Class itself.

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)

Of course:

   T'Class'Operational (X) => T'Operational (X)
   T'Class'Operational (X) => S'Operational (X)

From this you can formally analyse if initialization is correct.

> I believe that such dispatching may be quite useful in some designs,

Yes it is. This is why there must be a hook at the end of construction of
T'Class. The earliest point you can dispatch if when T'Class'Operational
turns true.

> just as re-dispatching is useful in some designs - IMO.

No. This is a totally different case.

> Moreover, I think this question of constructor/destructor control flow
> is separate from the general question of preventing access to
> uninitialized data.

? Initialization = construction. I don't see how are they different.
-----------------
* T'Operational (X) is true when the object X can operate as an instance of
T.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de