Re: Type_Invariant and Finalize

[Robert A Duff <bobduff@shell01.TheWorld.com>]

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