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=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,494ac732c5488b7f
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!y21g2000vba.googlegroups.com!not-for-mail
From: Rod Chapman <roderick.chapman@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK: What does it prove?
Date: Fri, 28 May 2010 06:55:18 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <80ef9ed5-fd1b-4f41-8df9-b74b690444be@y21g2000vba.googlegroups.com>
References: <4bffc379$0$2374$4d3efbfe@news.sover.net>
NNTP-Posting-Host: 217.205.167.137
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1275054918 12270 127.0.0.1 (28 May 2010 13:55:18
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 28 May 2010 13:55:18 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: y21g2000vba.googlegroups.com; posting-host=217.205.167.137;
	posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB; rv:1.9.1.9)
	Gecko/20100315 Firefox/3.5.9 (.NET CLR 3.5.30729),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:12126
Date: 2010-05-28T06:55:18-07:00
List-Id: <comp.lang.ada>

On May 28, 2:25=A0pm, "Peter C. Chapin" <pcc482...@gmail.com> wrote:

> It is common to talk about SPARK proofs but of course what the Simplifier=
 is
> actually proving are the verification conditions generated by the Examine=
r.
> Formally this leaves open the question of if those verification condition=
s
> have anything to do with reality or not. Ultimately, it seems to me, befo=
re
> one can formally prove anything about the behavior of a program one needs=
 a
> formal semantics for the programming language in question. It is my
> understanding that SPARK95 does not have a formal semantics.

Well..not quite.  The VC generator was constructed and very much
based on the formal semantics for SPARK83 that was
contstructed in the mid-1990s.  We have _lots_ of confidence
that this semantics is completely upwards-compatible
and consistent with the canonical semantics of Ada95 and
this SPARK95 SPARK2005.

Unfortunately, we did not have the funding to keep
that SPARK83 semantics up to date with new features that
were added later like modular types from Ada95, but these
are a fairly modest extension to the language.

There are also lots of assumptions tha underlie any
"proof" of anything - in our case the integrity of the compiler,
linker and the rest of the build environment, the
implementation of the target processor itself and many
other things.  While these are valid concerns, these
assumptions really do seem to hold up in the "real world" - i.e.
with our customers using real commercial compilers, microprocessors
and so on.

In short: it seems to work.
 - Rod Chapman, SPARK Team, Praxis

PS...if the SPARK traffic here really does get annoyingly high,
then perhaps we should create comp.lang.ada.spark?