[RFC] Relaxed initialization for SPARK

[clairedross]

Link to rich view:

https://github.com/AdaCore/ada-spark-rfcs/blob/topic/spark-relaxed-init/considered/rfc-spark-relaxed-init.rst

[yannickmoy]

I am of the opinion that 'Initialized should only be allowed inside ghost code (which includes assertions).

[ChrisBorden]

Here's a naive comment from an inexperience user (me). These are relative to Init_By_Proof. FWIW: Allows putting Relaxed_Initialization on a type or individual declaration: +1 - I like that I can use on declaration and don’t have to create subtype, but have the flexibility to add to a type also.

<We have considered using a pragma Annotate (GNATprove, Relaxed_Initialization, V); to mean that a variable V has relaxed initialization, but it was more cumbersome than an aspect, and was a bit complicated (and heavy) when applied to function parameters.> I agree that aspect is less cumbersome than annotate.

In general, I like the way this is heading.

[jklmnn]

How would arrays be handled with the aspect? Would it be possible to initialize different slices at different times and then prove that the whole array has been initialized? In regards to arrays I'd also like to be able to prove that

for I in Array_Object'Range loop
   Array_Object (I) := Some_Value;
end loop;

initializes an array.

[yannickmoy]

@jklmnn Array initialization with a simple loop over the array range is now considered as completely initialized after the loop. That was the case for some time when the array is constrained, it's been extended to the unconstrained case not long ago (and it is part of Community 2019). But this is only based on limited heuristics in flow analysis.

With the extension discussed under this PR, you'll be able to very precisely say that cells at such-and-such indexes of the array have been initialized, because you'll rely on the very precise and powerful mechanics of proof. See examples of that with our current prototype in test https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/RC17-014__init_by_proof