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

[digitig <digitig@gmail.com>]

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.