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

[Simon Wright <simon@pushface.org>]

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;