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.13.223.193 with SMTP id i184mr3711806ywe.33.1440100822105; Thu, 20 Aug 2015 13:00:22 -0700 (PDT) X-Received: by 10.182.120.40 with SMTP id kz8mr72020obb.12.1440100822071; Thu, 20 Aug 2015 13:00:22 -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!69no2404149qgi.0!news-out.google.com!f6ni284igi.0!nntp.google.com!x6no2598384igd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 20 Aug 2015 13:00:21 -0700 (PDT) In-Reply-To: <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> 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: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <0115fd12-4ddb-43e9-8e7d-75a95a97796e@googlegroups.com> Subject: Re: Problems with SPARK 2015 and XMLAda From: Serge Robyns Injection-Date: Thu, 20 Aug 2015 20:00:22 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:27533 Date: 2015-08-20T13:00:21-07:00 List-Id: On Thursday, 20 August 2015 18:38:18 UTC+2, Shark8 wrote: > Do you /NEED/ SPARK? Maybe, maybe not. But there are certain properties o= f software built with formal methods that are desirable -- like the aforeme= ntioned absence of exceptions. >From the discussion it is clear I don't need SPARK for my application. The= application will consume data from external possibly unreliable sources. = It will work with systems that can fail, etc. My attempt with SPARK was to= be able to prove correctness of major portions of the code. However, it i= s not a live critical software component. Yes, I was wrong with my assumpt= ions about SPARK. With regards to exceptions I haven't any but XMLAda does raise them when fa= iling to validate the XML file. I'm using a few access variables where my = *current* design pushes me to do so (there is an older post about it by me = in this group) but when reading the GNAT container packages I do see they a= re used there too. Exceptions are nice to handle certain kinds of failure = without requiring to burden complex error handling everywhere. In a databa= se application it is perfectly acceptable to rollback the transaction in su= ch case. Thanks for sharing your thoughts.