From: "Rod Chapman" <rod.chapman@praxis-his.com>
Subject: ANN: SPARK 7.3 now available
Date: 26 Jan 2006 06:20:09 -0800
Date: 2006-01-26T06:20:09-08:00 [thread overview]
Message-ID: <1138285209.453720.222910@g49g2000cwa.googlegroups.com> (raw)
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
reply other threads:[~2006-01-26 14:20 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox