Re: Quick question regarding limited type return syntax

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

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.

>> 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".

In Ada, the object is created and default-initialized (or initialized by
component-specific Initialize calls) before Initialize is called on it.
In this sense, construction in Ada is automatic, and Initialize is only
a "post-constructor" hook.

> 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.

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".

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. For example, the 'Class semantics may include
registration of all objects in some registry, but this registry may need
some object-specific data that depends on the particular type of the
object and is provided by a dispatching operation.

> 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.

>> 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. The reason can be that initialization is too
costly, and the initialization values are never used; or the reason can
be that the initialization could only assign dummy values, and therefore
would only ensure that later errors have a deterministic effect, but
could not ensure that no dummy initial values are used by mistake as
non-dummy values.

The canonical example is a large array that will be used as a stack, or
in which data blocks will be allocated and deallocated in some other
controlled way. Thus, the array is created (i.e. allocated or
constructed) but usually it still contains uninitialized and therefore
unpredictable data (at least in traditional processors and operating
systems -- some new or security-conscious systems have memory allocators
which do initialize all allocated memory areas, albeit with dummy values
such as zeros).

Such data structures usually have special components which "indicate"
which parts of the data structure are initialized and usable, and which
parts are not. For example, a stack pointer can perform this role for an
array that implements a stack. But current programming languages,
including Ada, do not provide any general support for this logical
connection between "indicators" and initialized/uninitialized data; the
connection must in each case be specifically formalized and then used to
prove that any data that is read has first been initialized (with real
values).

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). I don't know what form
this support should take, however.

As a partial analogy, discriminant checks for variant records in Ada
ensure that non-existent components are not accessed, but do not ensure
that the accessed components are initialized with useful values.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .