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: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!v102.xanadu-bbs.net!xanadu-bbs.net!nntp.club.cc.cmu.edu!micro-heart-of-gold.mit.edu!newsswitch.lcs.mit.edu!nntp.TheWorld.com!.POSTED!not-for-mail
From: Robert A Duff <bobduff@shell01.TheWorld.com>
Newsgroups: comp.lang.ada
Subject: Re: Type_Invariant and Finalize
Date: Fri, 18 Jul 2014 17:48:16 -0400
Organization: The World Public Access UNIX, Brookline, MA
Message-ID: <wccbnsm1gpr.fsf@shell01.TheWorld.com>
References: <slrnlsg4lu.i0l.lithiumcat@nat.rebma.instinctive.eu>
 <ly7g3byald.fsf@pushface.org>
 <slrnlshh8m.i0l.lithiumcat@nat.rebma.instinctive.eu>
NNTP-Posting-Host: shell01.theworld.com
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: pcls7.std.com 1405720068 13251 192.74.137.71 (18 Jul 2014 21:47:48
 GMT)
X-Complaints-To: abuse@TheWorld.com
NNTP-Posting-Date: Fri, 18 Jul 2014 21:47:48 +0000 (UTC)
User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix)
Cancel-Lock: sha1:zMN70PLrkUmhaHa9B5yuagv6LsM=
Xref: news.eternal-september.org comp.lang.ada:21050
Date: 2014-07-18T17:48:16-04:00
List-Id: <comp.lang.ada>

Natasha Kerensikova <lithiumcat@instinctive.eu> writes:

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

I suggest using predicates instead of "not null":

    type Optional_Element_Access is access all Element'Class;
    subtype Element_Access is Optional_Element_Access with
        Predicate => Element_Access /= null;

"Predicate" is gnat-specific.  Use "Dynamic_Predicate" if you want to be
portable.  You can mostly use Element_Access, but use
Optional_Element_Access in the rare cases (e.g. inside Finalize)
where you want to allow null.

One problem with "not null" is that you can't create an object, and then
initialize it later.  Consider:

    X : Positive;
    ... -- No reads of X here.
    X := Something(...); -- Here we initialize X to some value >= 1.
    ... -- Now we can read X.

That works fine.  But similar code doesn't work with "not null":

    X : Element_Access;
    ... -- No reads of X here.
    X := Something(...); -- Here we initialize X to some non-null value.
    ... -- Now we can read X.

If Element_Access is declared "not null", then the declaration of X
blows up.  Using a predicate instead, it works the same way as the
Positive example.

- Bob