Re: Problems with SPARK 2015 and XMLAda

[Jacob Sparre Andersen <sparre@nbi.dk>]

Serge Robyns wrote:

> Sadly I quickly abandoned SPARK [...]

> And I know many other things SPARK doesn't like, like exceptions [...]

One important purpose of SPARK is to avoid exceptions completely, so
yes.

> or access types.

Yes.  Proving a program using access types to be correct is rather
difficult.

> So I guess it must dislike the standard containers too.

Yes, but there are containers for SPARK too.

In general, you can't use much of the *Ada* standard libraries with
SPARK, as they aren't annotated for correctness proofs.

If you want to program in SPARK, you shouldn't try to write Ada, and
then just run a tool, when you're done.  You should read the SPARK LRM
(or a textbook on SPARK), and understand the language.

Greetings,

Jacob
-- 
"I have no prejudice except against Pakistanis, which is normal."