Re: Quick question regarding limited type return syntax

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

On Mon, 04 Aug 2014 22:37:27 +0300, Niklas Holsti wrote:

> On 14-08-04 15:43 , Dmitry A. Kazakov wrote:
>> 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.
> 
> Ok, I should have said "for similar purposes as constructors and
> destructors".
>
>> 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.
> 
> You have a certain concept of what a "constructor" should do, and should
> not do; the latter includes dispatching. Ada allows dispatching from
> Initialize, but you can disallow it by a personal design and coding rule.

No. I use the standard meaning of the constructor. Constructor is a thing
that makes a type instance from the chunk of raw memory.

Then I consider types T, S, T'Class, S'Class and conclude whether the
corresponding constructors could dispatch from within. This has nothing to
do with specifically Ada or with my personal choices.

>>> 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.
> 
> Depends on the meaning you assign to "constructor".

See above.

> In Ada, the object is created and default-initialized (or initialized by
> component-specific Initialize calls) before Initialize is called on it.

The object is allocated and initialized by whatever means. The second part
is called constructor. Initialize is a part of the constructor (a hook).

> In this sense, construction in Ada is automatic, and Initialize is only
> a "post-constructor" hook.

Yes. It is always so, because per definition a constrictor cannot be a
typed subprogram since it *changes* the object's type from nothing to a
distinct type. We can only hook it, as Initialize does. C++ "constructors'
are just hooks as well.
 
>> 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)
> 
> You have invented a boolean predicate "Operational". In practice,
> objects do not have only two states: "not operational" and
> "operational"; they have several states, and "initialization" is often a
> multi-step process which takes the object through a sequence of logical
> states, from its default-initialized state to whatever level of
> initialization is desired at this stage.

You could refine that in the terms of language types, I gave an example
when answering to Georg.

But presently Ada has it in the all-or-nothing form.

> For a well-worn example, a File object is usually born in a "closed"
> state, and is then "operational" only in a limited sense; later, opening
> the File makes it more "operational".

No. File_Type from Ada.Text_IO is operational in all its states = you are
allowed to use any operations of Ada.Text_IO on a closed file. No problem.

You could attempt to introduce a file type that were operational only when
open. In that case you would have to ensure it open before you leave the
constructor. You could not close it before running the destructor.

Formally speaking it is whether Is_Open is a part of the type invariant or
not.

> Some steps in the initialization process, while described in the
> semantics of the parent type (the 'Class), may need assistance that is
> specific to a derived type, and therefore dispatching from Initialize
> may be useful.

Nobody argues that dispatching from constructors were not useful. The point
is - dispatching from the constructor of WHAT?

You can dispatch only at the end of the constructor of T'Class. You cannot
dispatch nowhere from the constructor of T.

>> 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.
> 
> Only in your limited, two-state formalization, which IMO is not realistic.

Show me tree-state, four-state formalization. My sole requirement is, don't
break types, Ada is supposed to be a typed language.

>>> 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.
> 
> The point is that for some data structures, it is not desirable to
> initialize (= store data in) all allocated storage locations when the
> data structure is created.

They are still initialized with the garbage. No problem. You think of
initialization as of spending some CPU cycles. It is not. The only purpose
of initialization is to bring the type invariant up and thus to make the
object operational. The invariant can be just True.

> My aim was to complain about this lack of language support for such
> "indicators" and other features that help to prove that a program never
> uses uninitialized variables (nor dummy values).

This is an unrelated issue. An "uninitialized" object like:

   X : Integer;

is still fully constructed, operational and initialized, but not in the
sense of initialization you used = an explicit specification that the new
object must be in the state so and so.

> I don't know what form
> this support should take, however.

1. An ability do disallow default constructors, as it was done for
indefinite types:

   X : String; -- Illegal (no constructor)

2. Integration of SPARK. When you about prove X having certain value, the
prover will not be able to do that if the thing was never assigned.

3. Proper construction model. You must be able to write

   type ... is record
      P : not null access Something;

and then the compiler must require you to provide a constructor and add the
post-condition on P to it.

4. Proper construction model.

   X : T := Y;

must call to a constructor (hook) with the parameter Y.

5. Proper construction model.

   X : T (Y, Z);

must call to a constructor with the parameters (Y, Z).

6. Proper construction model.

   X : T := (Y, Z);

must call to a constructor with the parameters (Y, Z), *not* with an
aggregate.

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