Re: [Spark] Using defered constants

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

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

This is actually very difficult, since logically the private is
_is_ part of the body!  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.

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

Why not "type X is Integer'First .. Integer'Last;"?

This is legal SPARK, so no need to hide the private part at all.
 - Rod