[Spark] Using defered constants

[Spark] Using defered constants

[Lutz Donnerhacke]

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;

Re: [Spark] Using defered constants

[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

Re: [Spark] Using defered constants

[Lutz Donnerhacke]

* 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.

Re: [Spark] Using defered constants

[Hyman Rosen]

Lutz Donnerhacke wrote:
> It's an example. I need an access type there.

SPARK doesn't have access types, I hear. I'm told
that this is so that the correctness of the code
is easier to prove, and that code that needs access
types should be written in plain Ada.

Re: [Spark] Using defered constants

[Lutz Donnerhacke]

* Hyman Rosen wrote:
> Lutz Donnerhacke wrote:
>> It's an example. I need an access type there.
>
> SPARK doesn't have access types, I hear. I'm told that this is so that
> the correctness of the code is easier to prove, and that code that needs
> access types should be written in plain Ada.

Your ears are working fine. I can use a sufficient Integer type, too, but
playing with such brain damages is subject of the other side of the Spark
border. I only have to fullfill the API constraints. You may suggest to not
use Spark everytime, an enviroment is accessed, but this is clearly not an
option, because it requires the whole programm to be written in Ada not
Spark consequently.

OTOH my question does not deal with this topic, but with a Spark strangeness.
So please keep the ball in the field. Thank you.

PS: I use Spark to shrink the executable's size: By proofing the absence of
run time errors, I can drop the run time checks completely. In order to not
introduce those error handlers again in the patch code written in Ada, the
Ada parts has to be as simple as possible. That's why the mix is free from
run time errors despite I use glue code! (Otherwise the linker will complain.)

Re: [Spark] Using defered constants

[Vinzent Hoefler]

Hyman Rosen <hyrosen@mail.com> wrote:

>Lutz Donnerhacke wrote:
>> It's an example. I need an access type there.
>
>SPARK doesn't have access types, I hear. I'm told
>that this is so that the correctness of the code
>is easier to prove,

Yes.

>and that code that needs access
>types should be written in plain Ada.

"SPARK 95 - The SPADE Ada 95 Kernel" explicitely states:

|Any Ada feature which does not appear in SPARK can still be employed
|if the subprogram which makes use of it has its body hidden by means
|of a "hide" directive ...

So I guess that is exactly what the #hide is intended for.

Lutz simply tries to use as much SPARK as possible. I do not think,
there is anything wrong with that approach.


Vinzent.

Re: [Spark] Using defered constants

[Peter Amey]

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;

Re: [Spark] Using defered constants

[Lutz Donnerhacke]

* Peter Amey wrote:
> 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).

Thank you very much.

> 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".

Of course. You can't check hidden areas. If you would do so, you would not
need the argument of #hide, because then you can determine the closure of
the hidden region yourself.

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

I'm not an active user. I'm just playing with Spark and Ada.

Back to the original problem. A simple workaround is to replace the constant
by a parameterless (inlined) function.

package t is
   type x is private;
   function cx return x;
   procedure copy(o : out x; i : Integer);
   --# derives o from i;
private
   --# hide t;
   type x is new Integer;
end t;

package body t is
   function cx return x is
      --# hide cx;
   begin
      return 0;
   end cx;

   procedure doupdate(o : in out x; i : Integer)
     --# derives o from i, o;
     is
      --# hide doupdate;
   begin
      o := o + x(i);
   end doupdate;

   procedure copy(o : out x; i : Integer) is
   begin
      o := cx;
      doupdate(o, i);
   end copy;
end t;