Re: Problems with SPARK 2015 and XMLAda

[Shark8 <onewingedshark@gmail.com>]

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.