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: 103376,8844b3d7ebfd08cd,start
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!42g2000cwt.googlegroups.com!not-for-mail
From: roderick.chapman@googlemail.com
Newsgroups: comp.lang.ada
Subject: ANN: SPARK 7.4 now available
Date: 9 Jan 2007 06:28:01 -0800
Organization: http://groups.google.com
Message-ID: <1168352881.704969.14040@42g2000cwt.googlegroups.com>
NNTP-Posting-Host: 217.205.167.137
Mime-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
X-Trace: posting.google.com 1168352888 14671 127.0.0.1 (9 Jan 2007 14:28:08
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 9 Jan 2007 14:28:08 +0000 (UTC)
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.8.1.1) Gecko/20061204 Firefox/2.0.0.1,gzip(gfe),gzip(gfe)
Complaints-To: groups-abuse@google.com
Injection-Info: 42g2000cwt.googlegroups.com; posting-host=217.205.167.137;
   posting-account=EhC47gwAAABJYiJ7JUJjwDyYMTWH1OKq
Xref: g2news2.google.com comp.lang.ada:8100
Date: 2007-01-09T06:28:01-08:00
List-Id: <comp.lang.ada>

Praxis are pleased to announce the immediate availability of release
7.4
of the SPARK language and toolset.

Full details, including the toolset release note, are available from
www.sparkada.com
as usual.

Professional, supported customers will receive upgrades immediately.
Upgrade
packages for for readers of the SPARK Textbook are also available by
download
from http://www.praxis-his.com/sparkada/sparkbook.asp

Highlights of this release include:

    New "accept" annotation system to indicate that a particular error
or warning is expected and justified.

    New "Always_Valid" assertion to indicate that the values read from
an external input are trustworthy.

    Obsolete SPARK83 floating-point attributes are now acceptable in
SPARK95 mode.

    Better error messages for common syntax and semantic errors.

    Complete re-implementation of VC Generation for single- and
multi-dimensional unconstrained array parameters. Supporting
improvements in the default invariant generator and Simplifier.

    Conditional data- and information-flow anomalies are now reported
as errors not warnings.

    Support for System.Bit_Order and System.Default_Bit_Order in the
configuration file.

    The Examiner now issues a warning if an Ada2005 reserved word is
used as an identifier in SPARK95 mode.

    The Simplifier's handling is user-defined and Examiner-generated
proof-rules has been unified and improved.

    The Simplifier has a new family of proof tactics for enumerated and
integer inequalities where transitivity of the relational operators is
involved.

    The implementation of the /p=N (multiprocessor) switch in SPARKSimp
has been re-implemented to make much better use of all the available
processing resources on multi-core or multi-processor machines.

    SPARKFormat now has options to reformat the own, initializes and
inherit annotations.

    SPARKMake can now produce with absolute or relative pathnames in
the generated index and meta-files.

Yours,
 Rod Chapman and the SPARK Team, Praxis