Re: Problems with SPARK 2015 and XMLAda

[brbarkstrom@gmail.com]

An alternative to SPARK may be TLA+ and its associated
tools.  TLA+ has a lot of work put in by Leslie Lamport,
who won last year's ACM Turing prize.  The April issue
of Comm. ACM has a report from Amazon Web Service developers
about using TLA+ and its tools to provide formal methods
of proving that programs are correct:

Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M.,
and Dearduff, M., 2015: How Amazon Web Services Uses Formal
Methods, Comm. ACM, 58, No. 4, 66-73.

The tools are available using an Eclipse environment, which 
suggests that the tool developers are being supported by an IBM
contingent of developers.

I've not delved deeply into TLA+, which has a pretty
massive amount of hypertext documentation, see

Lamport, L., 2015: The TLA Home Page, <http:research.microsoft.com/
en-us/um/people/lamport/tla/tla.html>

Thus, I don't know how much of an advance these tools make 
over SPARK.  I can't say whether they support exceptions, access 
variables, or task hierarchies.  On the other hand, TLA+ is probably one 
generation beyond SPARK and Lamport has a very high reputation 
for his math.  It is clear that TLA+ and its tools support
preconditions and postconditions for assisting proofs.
Merging TLA+ with Ada is probably at about the same level
of difficulty as merging SPARK with Ada.  According to the
article on the Amazon experience, TLA+ is fairly easy to
learn.

Bruce B.