* Puzzled by SPARK global aspect
@ 2017-06-30 21:29 digitig
2017-07-01 15:51 ` Anh Vo
0 siblings, 1 reply; 5+ messages in thread
From: digitig @ 2017-06-30 21:29 UTC (permalink / raw)
Suppose in my package specification I have
type Quadrant_Specification_Array is
array(Global.Quadrant_X_Index'Range, Global.Quadrant_Y_Index'Range)
of Quadrant_Specification;
(With QuadrantSpecification being a record type) and in my package body I have:
function N_Total_Klingons return Global.Klingon_Counter
with
Refined_Global => (Input => Quadrant_Specifications)
is
Total: Global.Klingon_Counter := 0;
begin
for X in Quadrant_Specifications'Range loop
for Y in Quadrant_Specifications'Range(2) loop
Total := Total + Quadrant_Specifications(X, Y).N_Klingons;
end loop;
end loop;
return Total;
end N_Total_Klingons;
Spark gives me an error
useless refinement, subprogram "N_Total_Klingons" does not depend on abstract state with visible refinement
But if I take the Refined_Global specification out I get the error
"Quadrant_Specifications" must be listed in the Global aspect of "N_Total_Klingons"
I feel I'm losing either way - if I do specify it I'm wrong, if I don't specify it I'm wrong.
How *do* I fix this?
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Puzzled by SPARK global aspect
2017-06-30 21:29 Puzzled by SPARK global aspect digitig
@ 2017-07-01 15:51 ` Anh Vo
2017-07-01 18:25 ` digitig
0 siblings, 1 reply; 5+ messages in thread
From: Anh Vo @ 2017-07-01 15:51 UTC (permalink / raw)
On Friday, June 30, 2017 at 2:29:38 PM UTC-7, digitig wrote:
> Suppose in my package specification I have
>
> type Quadrant_Specification_Array is
> array(Global.Quadrant_X_Index'Range, Global.Quadrant_Y_Index'Range)
> of Quadrant_Specification;
>
> (With QuadrantSpecification being a record type) and in my package body I have:
>
> function N_Total_Klingons return Global.Klingon_Counter
> with
> Refined_Global => (Input => Quadrant_Specifications)
> is
> Total: Global.Klingon_Counter := 0;
> begin
> for X in Quadrant_Specifications'Range loop
> for Y in Quadrant_Specifications'Range(2) loop
> Total := Total + Quadrant_Specifications(X, Y).N_Klingons;
> end loop;
> end loop;
> return Total;
> end N_Total_Klingons;
>
> Spark gives me an error
> useless refinement, subprogram "N_Total_Klingons" does not depend on abstract state with visible refinement
>
> But if I take the Refined_Global specification out I get the error
>
> "Quadrant_Specifications" must be listed in the Global aspect of "N_Total_Klingons"
>
> I feel I'm losing either way - if I do specify it I'm wrong, if I don't specify it I'm wrong.
>
> How *do* I fix this?
It is pretty hard to suggest advice since it is not a complete minimal code. In addition, I rather see the code instead of guessing. I would say your codes involve package Abstract State aspect.
Anh Vo
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Puzzled by SPARK global aspect
2017-07-01 15:51 ` Anh Vo
@ 2017-07-01 18:25 ` digitig
2017-07-02 0:45 ` Anh Vo
0 siblings, 1 reply; 5+ messages in thread
From: digitig @ 2017-07-01 18:25 UTC (permalink / raw)
On Saturday, July 1, 2017 at 4:51:22 PM UTC+1, Anh Vo wrote:
> On Friday, June 30, 2017 at 2:29:38 PM UTC-7, digitig wrote:
> > Suppose in my package specification I have
> >
> > type Quadrant_Specification_Array is
> > array(Global.Quadrant_X_Index'Range, Global.Quadrant_Y_Index'Range)
> > of Quadrant_Specification;
> >
> > (With QuadrantSpecification being a record type) and in my package body I have:
> >
> > function N_Total_Klingons return Global.Klingon_Counter
> > with
> > Refined_Global => (Input => Quadrant_Specifications)
> > is
> > Total: Global.Klingon_Counter := 0;
> > begin
> > for X in Quadrant_Specifications'Range loop
> > for Y in Quadrant_Specifications'Range(2) loop
> > Total := Total + Quadrant_Specifications(X, Y).N_Klingons;
> > end loop;
> > end loop;
> > return Total;
> > end N_Total_Klingons;
> >
> > Spark gives me an error
> > useless refinement, subprogram "N_Total_Klingons" does not depend on abstract state with visible refinement
> >
> > But if I take the Refined_Global specification out I get the error
> >
> > "Quadrant_Specifications" must be listed in the Global aspect of "N_Total_Klingons"
> >
> > I feel I'm losing either way - if I do specify it I'm wrong, if I don't specify it I'm wrong.
> >
> > How *do* I fix this?
>
> It is pretty hard to suggest advice since it is not a complete minimal code. In addition, I rather see the code instead of guessing. I would say your codes involve package Abstract State aspect.
>
> Anh Vo
Here's a fairly minimal spec and body, then, which gives the problem I describe:
---- main.ads ----
package Main
with
SPARK_Mode => On
is
type Quadrant_Specification is record
N_Klingons: Integer := 0;
end record;
subtype Klingon_Counter is Integer range 0..20;
type Quadrant_Specification_Array is
array(1..8, 1..8)
of Quadrant_Specification;
function N_Total_Klingons return Integer
with
Global => null,
Depends => (N_Total_Klingons'Result => null),
Pre => True;
end Main;
---- Main.adb ----
package body Main
with
SPARK_Mode => On
is
Quadrant_Specifications: Quadrant_Specification_Array;
function N_Total_Klingons return Integer
-- with
-- Refined_Global => Quadrant_Specifications
is
Total: Integer := 0;
begin
for X in Quadrant_Specifications'Range loop
for Y in Quadrant_Specifications'Range(2) loop
Total := Total + Quadrant_Specifications(X, Y).N_Klingons;
end loop;
end loop;
return Total;
end N_Total_Klingons;
end Main;
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Puzzled by SPARK global aspect
2017-07-01 18:25 ` digitig
@ 2017-07-02 0:45 ` Anh Vo
2017-07-02 0:59 ` Anh Vo
0 siblings, 1 reply; 5+ messages in thread
From: Anh Vo @ 2017-07-02 0:45 UTC (permalink / raw)
On Saturday, July 1, 2017 at 11:25:20 AM UTC-7, digitig wrote:
> On Saturday, July 1, 2017 at 4:51:22 PM UTC+1, Anh Vo wrote:
> > On Friday, June 30, 2017 at 2:29:38 PM UTC-7, digitig wrote:
> Here's a fairly minimal spec and body, then, which gives the problem I describe:
>
> ---- main.ads ----
> package Main
> with
> SPARK_Mode => On
> is
> type Quadrant_Specification is record
> N_Klingons: Integer := 0;
> end record;
>
> subtype Klingon_Counter is Integer range 0..20;
>
> type Quadrant_Specification_Array is
> array(1..8, 1..8)
> of Quadrant_Specification;
>
>
> function N_Total_Klingons return Integer
> with
> Global => null,
> Depends => (N_Total_Klingons'Result => null),
> Pre => True;
>
> end Main;
>
> ---- Main.adb ----
> package body Main
> with
> SPARK_Mode => On
> is
> Quadrant_Specifications: Quadrant_Specification_Array;
>
> function N_Total_Klingons return Integer
> -- with
> -- Refined_Global => Quadrant_Specifications
> is
> Total: Integer := 0;
> begin
> for X in Quadrant_Specifications'Range loop
> for Y in Quadrant_Specifications'Range(2) loop
> Total := Total + Quadrant_Specifications(X, Y).N_Klingons;
> end loop;
> end loop;
> return Total;
> end N_Total_Klingons;
> end Main;
Both Global and Depends are under umbrella of Abstract_State at the package level. Therefore, Abstract_State must be defined below. Note that Package_State is an arbitrary name.
package body Main
with
SPARK_Mode => On,
Refined_State => (Package_State => Quadrant_Specifications)
is
-- ...
In addition, Global and Depends are defined below because this function depends on local global variable.
function N_Total_Klingons return Integer
with
Global => Package_State,
Depends => (N_Total_Klingons'Result => Package_State)
is
-- ...
In the package body Refined_State must be defined to use Quadrant_Specifications as shown below.
package body Main
with
SPARK_Mode => On,
Refined_State => (Package_State => Quadrant_Specifications)
is
-- ...
Moreover, Refined_Global and Refined_Depends aspects must be declared to use the array variable Quadrant_Specifications.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Puzzled by SPARK global aspect
2017-07-02 0:45 ` Anh Vo
@ 2017-07-02 0:59 ` Anh Vo
0 siblings, 0 replies; 5+ messages in thread
From: Anh Vo @ 2017-07-02 0:59 UTC (permalink / raw)
On Saturday, July 1, 2017 at 5:45:28 PM UTC-7, Anh Vo wrote:
> On Saturday, July 1, 2017 at 11:25:20 AM UTC-7, digitig wrote:
> > On Saturday, July 1, 2017 at 4:51:22 PM UTC+1, Anh Vo wrote:
> > > On Friday, June 30, 2017 at 2:29:38 PM UTC-7, digitig wrote:
> > Here's a fairly minimal spec and body, then, which gives the problem I describe:
> >
> > ---- main.ads ----
> > package Main
> > with
> > SPARK_Mode => On
> > is
> > type Quadrant_Specification is record
> > N_Klingons: Integer := 0;
> > end record;
> >
> > subtype Klingon_Counter is Integer range 0..20;
> >
> > type Quadrant_Specification_Array is
> > array(1..8, 1..8)
> > of Quadrant_Specification;
> >
> >
> > function N_Total_Klingons return Integer
> > with
> > Global => null,
> > Depends => (N_Total_Klingons'Result => null),
> > Pre => True;
> >
> > end Main;
> >
> > ---- Main.adb ----
> > package body Main
> > with
> > SPARK_Mode => On
> > is
> > Quadrant_Specifications: Quadrant_Specification_Array;
> >
> > function N_Total_Klingons return Integer
> > -- with
> > -- Refined_Global => Quadrant_Specifications
> > is
> > Total: Integer := 0;
> > begin
> > for X in Quadrant_Specifications'Range loop
> > for Y in Quadrant_Specifications'Range(2) loop
> > Total := Total + Quadrant_Specifications(X, Y).N_Klingons;
> > end loop;
> > end loop;
> > return Total;
> > end N_Total_Klingons;
> > end Main;
>
> Both Global and Depends are under umbrella of Abstract_State at the package level. Therefore, Abstract_State must be defined below. Note that Package_State is an arbitrary name.
package Main
with
SPARK_Mode => On, Abstract_State => Package_State
is
--...
function N_Total_Klingons return Integer
with
Global => Package_State,
Depends => (N_Total_Klingons'Result => Package_State);
end Main;
In the package body, the Refined_State must be defined to associated with the constituents Quadrant_Specifications as shown below.
> package body Main
> with
> SPARK_Mode => On,
> Refined_State => (Package_State => Quadrant_Specifications)
> is
> -- ...
>
> In addition, Global and Depends are defined below because this function depends on local global variable.
>
> function N_Total_Klingons return Integer
> with
> Global => Package_State,
> Depends => (N_Total_Klingons'Result => Package_State)
> is
> -- ...
>
> In the package body Refined_State must be defined to use Quadrant_Specifications as shown below.
>
> package body Main
> with
> SPARK_Mode => On,
> Refined_State => (Package_State => Quadrant_Specifications)
> is
> -- ...
>
> Moreover, Refined_Global and Refined_Depends aspects must be declared to use the array variable Quadrant_Specifications.
Sorry, I cut out some good part before hitting the send button. Please ignore the previously incomplete post. Below is the complete one.
Both Global and Depends are under umbrella of Abstract_State at the package level. Therefore, Abstract_State must be defined below. Note that Package_State is an arbitrary name.
package Main
with
SPARK_Mode => On, Abstract_State => Package_State
is
--...
function N_Total_Klingons return Integer
with
Global => Package_State,
Depends => (N_Total_Klingons'Result => Package_State);
end Main;
In the package body, the Refined_State must be defined to associated with the constituents Quadrant_Specifications as shown below.
package body Main
with
SPARK_Mode => On,
Refined_State => (Package_State => Quadrant_Specifications)
is
-- ...
In addition, Global and Depends are defined below because this function depends on local global variable.
function N_Total_Klingons return Integer
with
Global => Package_State,
Depends => (N_Total_Klingons'Result => Package_State)
is
-- ...
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2017-07-02 0:59 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-06-30 21:29 Puzzled by SPARK global aspect digitig
2017-07-01 15:51 ` Anh Vo
2017-07-01 18:25 ` digitig
2017-07-02 0:45 ` Anh Vo
2017-07-02 0:59 ` Anh Vo
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox