From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.99.108.4 with SMTP id h4mr1323819pgc.1.1498933519122; Sat, 01 Jul 2017 11:25:19 -0700 (PDT) X-Received: by 10.36.125.65 with SMTP id b62mr592479itc.5.1498933519049; Sat, 01 Jul 2017 11:25:19 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!2.eu.feeder.erje.net!feeder.erje.net!2.us.feeder.erje.net!news.ripco.com!news.glorb.com!v202no468383itb.0!news-out.google.com!k7ni5504itk.0!nntp.google.com!v202no468379itb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sat, 1 Jul 2017 11:25:18 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=82.8.94.50; posting-account=7NSrMAoAAACQXGDiUf5Zzn18ZM31fxb5 NNTP-Posting-Host: 82.8.94.50 References: <7f7a804e-b90d-4a60-b759-21ae14da3835@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <9d8c9cd9-f6b8-4ca3-859e-46f8c1ef019b@googlegroups.com> Subject: Re: Puzzled by SPARK global aspect From: digitig Injection-Date: Sat, 01 Jul 2017 18:25:19 +0000 Content-Type: text/plain; charset="UTF-8" Xref: news.eternal-september.org comp.lang.ada:47253 Date: 2017-07-01T11:25:18-07:00 List-Id: 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;