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-Thread: 103376,652d8bded057eafa,start
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!g49g2000cwa.googlegroups.com!not-for-mail
From: "Rod Chapman" <rod.chapman@praxis-his.com>
Newsgroups: comp.lang.ada
Subject: ANN: SPARK 7.3 now available
Date: 26 Jan 2006 06:20:09 -0800
Organization: http://groups.google.com
Message-ID: <1138285209.453720.222910@g49g2000cwa.googlegroups.com>
NNTP-Posting-Host: 217.205.167.130
Mime-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
X-Trace: posting.google.com 1138285214 26873 127.0.0.1 (26 Jan 2006 14:20:14
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 26 Jan 2006 14:20:14 +0000 (UTC)
User-Agent: G2/0.2
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.7.8) Gecko/20050511 Firefox/1.0.4,gzip(gfe),gzip(gfe)
Complaints-To: groups-abuse@google.com
Injection-Info: g49g2000cwa.googlegroups.com; posting-host=217.205.167.130;
   posting-account=EhC47gwAAABJYiJ7JUJjwDyYMTWH1OKq
Xref: g2news1.google.com comp.lang.ada:2648
Date: 2006-01-26T06:20:09-08:00
List-Id: <comp.lang.ada>

Praxis High Integrity Systems are pleased to announce the
immediate availability of release 7.3 of the SPARK language
and toolset.

Complete details, including the revised languauge definition
and the toolset release note are now available from www.sparkada.com

Supported customers are being upgraded now. Academic users
and tool-partners will be upgraded shortly.

Tool upgrade packages for readers of the SPARK textbook are
also available from www.sparkada.com

Highlights of this release include:

    VC Generation improvements in the presence of
    semantic and data-flow errors.

    Support for full-range of IEEE 64-bit floating point values
    in the configuration file.

    A new Examiner switch that produces explanations of
    errors and warnings on-screen and in the listing files.

    Better error messages for common syntax errors.

    Relaxation of the rule requiring qualification of modular literals.

    Support for proof rules involving the 'Size attribute.

    Correct order or declaration in FDL files for type-announced
    and private types.

    Support for the use of pragma Import to complete an external
    own variable.

    Significant new Simplifier tactics for modular and rational
    inequalities.

    Support for user-defined proof rules for the Simplifier.

    Port of the Simplifier and Checker to the SICSTUS PROLOG
    compiler. Both are significantly faster as a result.

See www.sparkada.com for more details, including performance
metrics for the new Simplifier.

Yours,
 The SPARK Team, Praxis High Integrity Systems