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.68.102.99 with SMTP id fn3mr2978816pbb.2.1440088697626; Thu, 20 Aug 2015 09:38:17 -0700 (PDT) X-Received: by 10.182.81.130 with SMTP id a2mr51418oby.30.1440088697592; Thu, 20 Aug 2015 09:38:17 -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!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!news.ripco.com!news.glorb.com!se8no7112459igc.0!news-out.google.com!f6ni160igi.0!nntp.google.com!x6no2513829igd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 20 Aug 2015 09:38:17 -0700 (PDT) In-Reply-To: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=75.161.23.130; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 75.161.23.130 References: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> Subject: Re: Problems with SPARK 2015 and XMLAda From: Shark8 Injection-Date: Thu, 20 Aug 2015 16:38:17 +0000 Content-Type: text/plain; charset=ISO-8859-1 Xref: news.eternal-september.org comp.lang.ada:27530 Date: 2015-08-20T09:38:17-07:00 List-Id: On Wednesday, August 19, 2015 at 3:22:44 PM UTC-6, Serge Robyns wrote: > > I'm not going to waste my time fighting SPARK and put my trust in the standard ADA features and testing. To bad not being able to proof. How you've worded this makes me think that perhaps you think of SPARK as an extension of Ada [as superset], and that'll get you into a lot of headaches because SPARK is a subset of Ada [along w/ tools]. As others have said, SPARK is about avoiding exceptions completely (because the relevant properties are proved) and therefore having exceptions in your SPARK code is not allowed. Do you /NEED/ SPARK? Maybe, maybe not. But there are certain properties of software built with formal methods that are desirable -- like the aforementioned absence of exceptions.