Re: Problems with SPARK 2015 and XMLAda

[Serge Robyns <serge.robyns@gmail.com>]

On Thursday, 20 August 2015 18:38:18 UTC+2, Shark8  wrote:

> 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.

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 is not a live critical software component.  Yes, I was wrong with my assumptions about SPARK.

With regards to exceptions I haven't any but XMLAda does raise them when failing 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 are used there too.  Exceptions are nice to handle certain kinds of failure without requiring to burden complex error handling everywhere.  In a database application it is perfectly acceptable to rollback the transaction in such case.

Thanks for sharing your thoughts.