Re: Problems with SPARK 2015 and XMLAda

[Peter Chapin <PChapin@vtc.vsc.edu>]

On Thu, 20 Aug 2015, Shark8 wrote:

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

To clarify, SPARK 2014 does allow raise statements in programs. However, 
each Raise statement carries with it a proof obligation that it will never 
execute. What's the point of that? It allows you to use raise statements 
to document "impossible" situations and then have the tools attempt to 
prove that those situations are, indeed, impossible.

SPARK 2014 does not allow exception handlers, however.

Peter