Re: [Spark] Using defered constants

[Lutz Donnerhacke <lutz@iks-jena.de>]

* Rod Chapman wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:>    7  private
>>    8     --# hide t;
>>    9     type x is new Integer;
>>   10     cx : constant x := 0;
>>   11  end t;
>
> Tricky!  You are trying to arrange a package as follows:
>    Visible spec: SPARK
>    Private part of spec: hidden, Ada95
>    Body: SPARK

Ack.

> This is actually very difficult, since logically the private is
> _is_ part of the body!

But the initialisation of deferred constants is elaborated before the body
of the package. It's impossible to move the initialisation into the body
itself. Therefore the examiner must assume, that the hidden part will
initialisation the deferred constant.

> In partiular, the Examiner does not assume anything much about the
> content of the private part when analysing the body, hence the error that
> you're seeing.

Bad. Sad.

> Obvious point: why "type x is new Integer;"??  Do you really
> need an explicit derived type there?

It's an example. I need an access type there.