Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014

Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014

[digitig]

In main.ads I have:

package Main
with SPARK_Mode => On
is
   procedure Test;
end Main;

In main.adb I have:

with Ada.Numerics.Discrete_Random;
with Ada.Text_IO;
package body Main
with SPARK_Mode => On
is
   procedure Test is
      subtype Die is Integer range 1 .. 6;
      subtype Dice is Integer range 2*Die'First .. 2*Die'Last;
      package Random_Die is new Ada.Numerics.Discrete_Random (Die);
      use Random_Die;
      G : Generator;
      D : Dice;
   begin
      Reset (G);  -- Start the generator in a unique state in each run
      loop
         -- Roll a pair of dice; sum and process the results
         D := Random(G) + Random(G);
         Ada.Text_IO.Put_Line(D'Image);
      end loop;
   end Test;
end Main;

Running SPARK | Examine all sources from GPS gives me the error:

        9:7 "Random_Die" is not a library-level package
        9:7 incorrect placement of aspect "Spark_Mode"
        9:7 instantiation error at a-nudira.ads:45

Line 9 is:

      package Random_Die is new Ada.Numerics.Discrete_Random (Die);

But the error points into a line in the GNAT library, in a-nudira.ads that simply says

        SPARK_Mode => Off

I'm completely bewildered here - what's wrong with my code here (other than it being a toy example)? And how *do* I use Ada.Numerics.Discrete_Random in conjunction with SPARK?

Re: Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014

[Simon Wright]

digitig <digitig@gmail.com> writes:

> package body Main
> with SPARK_Mode => On
> is
>    procedure Test is
>       subtype Die is Integer range 1 .. 6;
>       subtype Dice is Integer range 2*Die'First .. 2*Die'Last;
>       package Random_Die is new Ada.Numerics.Discrete_Random (Die);

(SPARK GPL 2017) move these declarations up to package level .. then,

>       use Random_Die;
>       G : Generator;

 "Generator" is not allowed in SPARK
 violation of aspect SPARK_Mode at line xx

>       D : Dice;
>    begin
>       Reset (G);  -- Start the generator in a unique state in each run
>       loop
>          -- Roll a pair of dice; sum and process the results
>          D := Random(G) + Random(G);

 "Result_Subtype" is not allowed in SPARK
 violation of aspect SPARK_Mode at line xx

>          Ada.Text_IO.Put_Line(D'Image);
>       end loop;
>    end Test;
> end Main;

Re: Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014

[digitig]

On Friday, June 30, 2017 at 8:28:27 AM UTC+1, Simon Wright wrote:
> digitig writes:
> 
> > package body Main
> > with SPARK_Mode => On
> > is
> >    procedure Test is
> >       subtype Die is Integer range 1 .. 6;
> >       subtype Dice is Integer range 2*Die'First .. 2*Die'Last;
> >       package Random_Die is new Ada.Numerics.Discrete_Random (Die);
> 
> (SPARK GPL 2017) move these declarations up to package level .. then,
> 
> >       use Random_Die;
> >       G : Generator;
> 
>  "Generator" is not allowed in SPARK
>  violation of aspect SPARK_Mode at line xx
> 
> >       D : Dice;
> >    begin
> >       Reset (G);  -- Start the generator in a unique state in each run
> >       loop
> >          -- Roll a pair of dice; sum and process the results
> >          D := Random(G) + Random(G);
> 
>  "Result_Subtype" is not allowed in SPARK
>  violation of aspect SPARK_Mode at line xx
> 
> >          Ada.Text_IO.Put_Line(D'Image);
> >       end loop;
> >    end Test;
> > end Main;

But at least I can then turn SPARK-Mode off for the Test procedure, which means with a bit of shuffling I should be able to localise the part where SPARK-Mode is off to just the random number generator. Thanks.

I'm puzzled by why I have to do that, though, when Ada.Numerics.Discrete_Random itself turns SPARK_Mode off.