Re: [Spark] Using defered constants

[Peter Amey <peter.amey@praxis-cs.co.uk>]

This one is down to a decision I made years ago.  If the full definition 
of a private type is hidden then there is some uncertainty about what 
element types it contains and that has implications for the analysis the 
Examiner can do.  It seemed to me that I shouldn't make assumptions 
about what might be in the hidden private part of a package and 
therefore shouldn't allow the use of that type (and hence deferred 
constants of that type) in the subsequent package body.  In general it 
seemed that if the private part of the package spec was hidden then the 
body was unlikely to be legal SPARK either.

Lutz's question has caused me to reconsider all this and the next 
release of the Examiner will relax these rules so that after the point 
that Ada requires that the deferred constant to be complete it can be 
used even if the SPARK Examiner has not seen it (because it is hidden).

The worst consequence for the Examiner will be the ability to construct 
programs with hidden pakcage private parts that will examine cleanly but 
not compile because soemthing in the hidden part makes them illegal Ada; 
at least this is "safe".

As with all these things, it is feedback from active users that drive 
things forward!

Peter

Lutz Donnerhacke wrote:
> The following error does not make much sense for me. Any workaround?
> 
> $ cat example.lst
> Line
>    1  
>    2  package t is
>    3     type x is private;
>    4     cx : constant x;
>    5     procedure copy(o : out x; i : Integer);
>    6     --# derives o from i;
>    7  private
>    8     --# hide t;
>    9     type x is new Integer;
>   10     cx : constant x := 0;
>   11  end t;
>   12  
>   13  package body t is
>   14     procedure doupdate(o : in out x; i : Integer)
>   15       --# derives o from i, o;
>   16       is
>   17        --# hide doupdate;
>   18     begin
>   19        o := o + x(i);
>   20     end doupdate;
>   21     
>   22     procedure copy(o : out x; i : Integer) is
>   23     begin
>   24        o := cx;
>                  ^3
> *** (  3)  Semantic Error:611: Illegal use of deferred constant prior to its 
>            full declaration.
> 
>   25        doupdate(o, i);
>   26     end copy;
>   27  end t;