Re: Problems with SPARK 2015 and XMLAda

["Randy Brukardt" <randy@rrsoftware.com>]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com...
...
> 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.

One use of exceptions is to signal errors with the parameters of a 
routine -- essentially the failure of a precondition. Clearly, it is better 
that such things are proved impossible, and thus such exceptions are not 
needed in SPARK.

But another use of exceptions is to signal things that cannot be known at 
compile time. How can you tell in advance whether the file Foobar.Txt exists 
on your disk? Even a pretesting it is unreliable (it could be deleted 
between the test and the usage); one has to report the error at runtime.

SPARK forces such errors to be reported as error codes, and that's pure 
evil. The problems with using error codes rather than exceptions to report 
unlikely but possible errors are well-known, and forcing one to use that is 
essentially junking decades of programming experience.

The lack of access types is similar; one has to emulate them using arrays in 
SPARK, which is a 1950s programming technique. It's the sort of thing that 
one uses Ada to get way from.

At least the SPARK team is aware of these limitations and considering ways 
to mitigate them in future versions of SPARK. What I hate is people spinning 
these as "features" rather than just a limitation of prover technology (and 
to me, an indication that SPARK tries to do too much).

                            Randy.