Type_Invariant and Finalize

[Natasha Kerensikova <lithiumcat@instinctive.eu>]

Hello,

I have been trying out the new contrat-oriented aspects on Ada 2012, and
wondered how Type_Invariant interacts with user-defined finalization.

I have several types for which a Type_Invariant makes sense (and is
often already mostly implemented the old-fashionned way, with pragma
Assert at the end of subprograms), except after the first call to
Finalize.

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'm already a bit uneasy with not having "not null except after
Finalize" access types, but in the example above after the first call to
Finalize I get an array of either null or invalid access values, and the
natural type invariant can't be computed.

Searching through the ARM, I can't see any special treatment of the
Finalize procedure with regard to Type_Invariant aspect, so presumably
the type inveriant is also checked at the end of Finalize.

Have I missed something that allows Finalize to make an object not fit
the type invariant?

Or should I prepare for it, e.g. with an explicit boolean record
component that is False for the most of the lifetime of the object,
until the first call to Finalize?


Thanks in advance for your insights,
Natasha