From: Anh Vo <anhvofrcaus@gmail.com>
Subject: Re: Puzzled by SPARK global aspect
Date: Sat, 1 Jul 2017 08:51:20 -0700 (PDT)
Date: 2017-07-01T08:51:20-07:00 [thread overview]
Message-ID: <fa7e6ff7-8d53-48ad-a45e-3088b7b63d42@googlegroups.com> (raw)
In-Reply-To: <7f7a804e-b90d-4a60-b759-21ae14da3835@googlegroups.com>
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
next prev parent reply other threads:[~2017-07-01 15:51 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 [this message]
2017-07-01 18:25 ` digitig
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