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
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.albasani.net!uucp.gnuu.de!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Mon, 05 May 2014 18:40:11 +0200
From: "G.B." <rm-dash-bau-haus@dash.futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:24.0) Gecko/20100101 Thunderbird/24.4.0
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: I'm a noob here.
References: <2c400962-3a09-4da2-9f56-b4f1986b80f8@googlegroups.com>
 <42945a0c-e4ae-41ff-a2ce-d3faf41336ce@googlegroups.com>
 <c5be2835-dbb0-490d-a484-19c1a252a175@googlegroups.com>
In-Reply-To: <c5be2835-dbb0-490d-a484-19c1a252a175@googlegroups.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <5367beeb$0$6706$9b4e6d93@newsspool2.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 05 May 2014 18:40:11 CEST
NNTP-Posting-Host: ae1a7c2a.newsspool2.arcor-online.net
X-Trace: 
 DXC=HL=_RXME5c`;iVb[J9ZZP`A9EHlD;3Ycb4Fo<]lROoRa8kF<OcfhCOkC=LIOMLmjO`nc\616M64>jLh>_cHTX3jmSR]9580EM=e
X-Complaints-To: usenet-abuse@arcor.de
Xref: news.eternal-september.org comp.lang.ada:19692
Date: 2014-05-05T18:40:11+02:00
List-Id: <comp.lang.ada>

On 05.05.14 15:52, sdalemorrey@gmail.com wrote:
> On Monday, May 5, 2014 6:43:50 AM UTC-6, Dan'l Miller wrote:
>> In brief, what the OP is asking is:  precisely how does a SPARK compiler actually utilize the meta-information annotations?  E.g., precisely how does a SPARK compiler make logical inferences regarding correctness of Ada-subset source code to verify that the imperative code does what the annotations have declared?
>
> Well there is that and then there is the more general question of "What is the relationship of Ada to Spark" is one a subset or superset of the other?

To those unfortunate ones who cannot buy this information
about Ada vs SPARK from AdaCore,

    SPARK (originally) defines a subset of the Ada language
    in such a way that the absence of a class of errors can
    be proved mathematically, with the help of SPARK tools.

Think "lint on formal steroids".

SPARK's analysis needs more information that is available in a
typical Ada program, and this information is added in formal
comment syntax. Being comments, an Ada compiler will ignore them.
Being formal comments, SPARK tools will interpret the formal
comments as they apply to the program text proper.

More recently, AdaCore has integrated SPARK with Ada 2012,
in such a way that their recent Ada toolset can provide the
same functionality as SPARK, thereby removing the need
to have SPARK tools plus any Ada compiler, basically letting you
do the work with AdaCore's recent GNAT.

> Is every valid Spark program a valid Ada program,

Yes.

> or is every valid Ada program also a valid Spark program?

No, since SPARK restricts the Ada language.

> Ada documentation seems to be a bit thin, but Spark documentation has been nearly impossible to track down.  To my mind this means I'm either asking the question wrong, or asking the wrong question.
>
> A good primer on Spark as well as what tools I would need to see Spark in it's full glory would be a good place for me to start I believe.

There is quite a bit of documentation, including examples,
in the distributions themselves.