From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 border1.nntp.dca1.giganews.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!eu.feeder.erje.net!eternal-september.org!feeder.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Natasha Kerensikova <lithiumcat@instinctive.eu>
Newsgroups: comp.lang.ada
Subject: Re: Type_Invariant and Finalize
Date: Fri, 18 Jul 2014 06:56:23 +0000 (UTC)
Organization: A noiseless patient Spider
Message-ID: <slrnlshh8m.i0l.lithiumcat@nat.rebma.instinctive.eu>
References: <slrnlsg4lu.i0l.lithiumcat@nat.rebma.instinctive.eu>
 <ly7g3byald.fsf@pushface.org>
Injection-Date: Fri, 18 Jul 2014 06:56:23 +0000 (UTC)
Injection-Info: mx05.eternal-september.org;
 posting-host="76a49b86bc3e16725b7cfca3d85cb4c8";
 logging-data="32241"; mail-complaints-to="abuse@eternal-september.org";
 posting-account="U2FsdGVkX19e1albjs5zW593pTIcMIMV"
User-Agent: slrn/1.0.1 (FreeBSD)
Cancel-Lock: sha1:YdoN7GVR9ciR77XmAwVPVjk4a0E=
Xref: number.nntp.dca.giganews.com comp.lang.ada:187690
Date: 2014-07-18T06:56:23+00:00
List-Id: <comp.lang.ada>

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