Re: Type_Invariant and Finalize

[Natasha Kerensikova <lithiumcat@instinctive.eu>]

On 2014-07-17, Simon Wright <simon@pushface.org> wrote:
> Natasha Kerensikova <lithiumcat@instinctive.eu> writes:
>
>> The latest example is a sorted array of non-null
>> paccess-to-indefinite-type values, where the "sortedness" is a natural
>> type inveriant, but in Finalize I release the memory using an instance
>> of Unchecked_Deallocation.
>
> I don't think these can be null-excluding access types, because you
> can't instantiate Unchecked_Deallocation for such a type?

Probably, though I admit I haven't tried, because it feels so obvious it
somehow won't work.

In the part you quoted, "non-null" was not referring to null exclusion,
but rather to the fact that in normal operation the values in the array
happen to not be null.

I have been toying with the idea of putting the null exclusion in the
record component or array declaration:

   type Array_Of_Indefinite_Elements is array (Index range <>)
     of not null Element_Access;

   type Node is record
      Key : not null Key_Access;
      Element : not null Element_Access;
   end record;

Such declarations would have helped catch a few bugs I encountered, so I
find the idea desirable. However it makes Finalize a bit messy: I can
use an instance of Unchecked_Deallocation on an intermediate variable,
and then the array/record has an invalid access value instead of a null
one, which is fine as long as nothing tries to dereference or free it,
so I can't use directly a Type_Invariant (unless there is some special
provision about Finalize that I missed, which is the whole question of
the thread), and Finalize idempotency has to be ensured in some other
way (e.g. with a Finalized boolean component).

But these are a lot of hassle for a very limited corner case (whatever
happens between the first call to Finalize and the last use of the
object). So I wish there was some way to have not-null-except-during-
finalization access types, and Type_Invariant_Except_During_Finalization
and *_Predicate_Except_During__Finalization aspects.

Doesn't it make sense to weaken these restrictions/contracts in such a
very specific and limited part of the object lifetime?


Natasha