From: digitig <digitig@gmail.com>
Subject: Re: Puzzled by SPARK global aspect
Date: Sat, 1 Jul 2017 11:25:18 -0700 (PDT)
Date: 2017-07-01T11:25:18-07:00 [thread overview]
Message-ID: <9d8c9cd9-f6b8-4ca3-859e-46f8c1ef019b@googlegroups.com> (raw)
In-Reply-To: <fa7e6ff7-8d53-48ad-a45e-3088b7b63d42@googlegroups.com>
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;
next prev parent reply other threads:[~2017-07-01 18:25 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-06-30 21:29 Puzzled by SPARK global aspect digitig
2017-07-01 15:51 ` Anh Vo
2017-07-01 18:25 ` digitig [this message]
2017-07-02 0:45 ` Anh Vo
2017-07-02 0:59 ` Anh Vo
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox