From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.66.63.39 with SMTP id d7mr6965121pas.20.1440168339001;
        Fri, 21 Aug 2015 07:45:39 -0700 (PDT)
X-Received: by 10.182.105.130 with SMTP id gm2mr126633obb.13.1440168338962;
 Fri, 21 Aug 2015 07:45:38 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!x6no2936137igd.0!news-out.google.com!nt1ni10968igb.0!nntp.google.com!se8no7740032igc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 21 Aug 2015 07:45:38 -0700 (PDT)
In-Reply-To: <mr7a1b$psv$1@dont-email.me>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=50.111.152.65;
 posting-account=Ies7ywoAAACcdHZMiIRy0M84lcJvfxwg
NNTP-Posting-Host: 50.111.152.65
References: <e3de50ce-e994-4038-8160-13266aeb207e@googlegroups.com>
 <lymvxn112j.fsf@pushface.org>
 <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com>
 <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com>
 <mr5dnn$ce9$1@loke.gir.dk>
 <alpine.DEB.2.20.1508210804480.22981@debian>
 <puak04qc3k8o$.1epetyorakzeg$.dlg@40tude.net>
 <alpine.DEB.2.20.1508210948320.23241@debian>
 <1s0gzs5wzjtq2$.1kuy63rfjsov0.dlg@40tude.net>
 <mr6ta0$aq3$1@dont-email.me> <1j3alqfkzrx0r$.1gv7vbgpembl4$.dlg@40tude.net>
 <mr7a1b$psv$1@dont-email.me>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <738fc9dd-edee-41ca-bcc7-4af8a113d538@googlegroups.com>
Subject: Re: Problems with SPARK 2015 and XMLAda
From: brbarkstrom@gmail.com
Injection-Date: Fri, 21 Aug 2015 14:45:38 +0000
Content-Type: text/plain; charset=ISO-8859-1
Xref: news.eternal-september.org comp.lang.ada:27555
Date: 2015-08-21T07:45:38-07:00
List-Id: <comp.lang.ada>

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.