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.182.248.228 with SMTP id yp4mr1298088obc.24.1440019363162; Wed, 19 Aug 2015 14:22:43 -0700 (PDT) X-Received: by 10.140.102.243 with SMTP id w106mr197381qge.40.1440019363135; Wed, 19 Aug 2015 14:22:43 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!x6no2184169igd.0!news-out.google.com!78ni16762qge.1!nntp.google.com!69no2169028qgi.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 19 Aug 2015 14:22:42 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=85.201.165.65; posting-account=6m7axgkAAADBKh082FfZLdYsJ24CXYi5 NNTP-Posting-Host: 85.201.165.65 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> Subject: Re: Problems with SPARK 2015 and XMLAda From: Serge Robyns Injection-Date: Wed, 19 Aug 2015 21:22:43 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:27513 Date: 2015-08-19T14:22:42-07:00 List-Id: Hi Simon, Manually editing the grp file as suggested did the trick. Sadly I quickly abandoned SPARK as it barked on me for using bounded string= s. I intend to use a DB with my application and bounded strings seems to b= e the way to go, even if I do find them a pain to use. For every type of s= tring I've to instantiate the generic package as I want to have strong typi= ng on the usage of these strings throughout the program and this is one of = my drivers to use Ada. And I know many other things SPARK doesn't like, like exceptions (not used = (yet)) or access types. So I guess it must dislike the standard containers= too. I guess I'll uninstall SPARK, as so far it hasn't been so helpful for me. For example in another small toy (a little game) I'm using the following co= nstruct. Count1 : Natural range 0 .. Number_Of_Columns; Count2 : Natural range 0 .. Number_Of_Columns; The_Score : Integer :=3D 0; J : Columns; -- To speed up, the value is calculated as a delta -- from the previous value. -- This is the less good code of this game (I'm not proud). begin -- -- Horizontal -- Count1 :=3D 0; if Column > Columns'First then for J in reverse Columns'First .. Columns'Pred (Column) loop exit when The_Board.Board (Row, J) /=3D Player; Count1 :=3D Count1 + 1; pragma Loop_Invariant ( Count1 <=3D Number_Of_Columns - Integer= (Columns'First - Columns'Pred (Column))); pragma Loop_Variant ( Increases =3D> Count1 ); pragma Loop_Variant ( Decreases =3D> J ); end loop; end if; Count2 :=3D 0; if Column < Columns'Last then for J in Columns'Succ (Column) .. Columns'Last loop exit when The_Board.Board (Row, J) /=3D Player; Count2 :=3D Count2 + 1; pragma Loop_Invariant ( Count2 < Number_Of_Columns ); pragma Loop_Variant ( Increases =3D> Count2 ); pragma Loop_Variant ( Increases =3D> J ); end loop; end if; SPARK warns about potential range errors on Count1 and Count2 while I've pu= t a lot of safeguards and tried two different Loop_Invariant constructs to = tell SPARK to be happy. For every construct attempt I get a different erro= r. I'm not going to waste my time fighting SPARK and put my trust in the stand= ard ADA features and testing. To bad not being able to proof. Serge