* Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014
@ 2017-06-30 1:15 digitig
2017-06-30 7:28 ` Simon Wright
0 siblings, 1 reply; 3+ messages in thread
From: digitig @ 2017-06-30 1:15 UTC (permalink / raw)
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?
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014
2017-06-30 1:15 Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014 digitig
@ 2017-06-30 7:28 ` Simon Wright
2017-06-30 11:38 ` digitig
0 siblings, 1 reply; 3+ messages in thread
From: Simon Wright @ 2017-06-30 7:28 UTC (permalink / raw)
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;
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014
2017-06-30 7:28 ` Simon Wright
@ 2017-06-30 11:38 ` digitig
0 siblings, 0 replies; 3+ messages in thread
From: digitig @ 2017-06-30 11:38 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2017-06-30 11:38 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-06-30 1:15 Can't work out how to use with Ada.Numerics.Discrete_Random with SPARK 2014 digitig
2017-06-30 7:28 ` Simon Wright
2017-06-30 11:38 ` digitig
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox