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=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,7735ba83f2314b34,start
X-Google-Attributes: gid103376,public
Path: g2news1.google.com!postnews1.google.com!not-for-mail
From: rod.chapman@praxis-cs.co.uk (Rod Chapman)
Newsgroups: comp.lang.ada
Subject: ANN: SPARK Book release 7.1 upgrades...
Date: 4 Jun 2004 08:49:15 -0700
Organization: http://groups.google.com
Message-ID: <cf2c6063.0406040749.3d7cae14@posting.google.com>
NNTP-Posting-Host: 62.173.119.178
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1086364155 6241 127.0.0.1 (4 Jun 2004 15:49:15
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 4 Jun 2004 15:49:15 +0000 (UTC)
Xref: g2news1.google.com comp.lang.ada:1098
Date: 2004-06-04T08:49:15-07:00
List-Id: <comp.lang.ada>

We're pleased to announce the availability of
release 7.1 of the SPARK Toolset for purchasers of
the "SPARK Book" by John Barnes.

These are available now for Windows and IA32/Linux
from www.sparkada.com

This release includes the SPARK Examiner version 7.1
and Simplifier 2.15.  The latter includes signigicant
improvements to its theorem proving tactics for
VCs involving quantifiers and updates to composite
objects (e.g. arrays).

The language and Examiner 7.1 support the recent
"RavenSPARK" tasking features of SPARK.

Full documentation is included in each of the packages.

All the best,
 Rod Chapman, SPARK Team, Praxis Critical Systems