ANN: SPARK 7.3 now available

ANN: SPARK 7.3 now available

[Rod Chapman]

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