ANNOUNCE: SPARK toolset 6.1 now available

[rod@praxis-cs.co.uk (Rod Chapman)]

Praxis Critical Systems is pleased to announce
the immediate availability of release 6.1 of
the SPARK language and the SPARK toolset.

Commercial supported customers will receive their
upgrades within the next few weeks.  Tool partners
and academic users will be upgraded following that.
A new release for readers of John Barnes' "SPARK Book"
will be available soon.

The full release note is available on-line at www.sparkada.com

The full definition of SPARK ("The SPARK Report") is
also available to interested parties upon request.

Release 6.1 of the SPARK language adds:

  - A useful subset of Ada95's tagged types are now permitted
    in SPARK95.  Inheritance and extension of tagged types are
    allowed, as is the overriding of basic operations.  Dispatching
    operations are not permitted.

  - A new "type assertion" annotation can be used to specify the
    predefined base type from which an integer type declaration
    is derived.  A complementary configuration-file mechanism allows
    a user to specify the details of packages Standard and System for
    a particular implementation.  When used together, these facilities
    greatly improve the Simplifier's ability to discharge run-time
    exceptions verification conditions arising from Overflow_Check
    in both SPARK83 and SPARK95.

  - Both full-range and constrained subtypes of modular types are
    now permitted in SPARK95.

There are also significant enhancements to the Examiner, Simplifier
and Checker with this release.  Highlights include:

  - When the configuration file mechanism is used to specify packages
    Standard and System, the Examiner can check a number of additional
    static semantic rules of Ada.  This also improves VC generation
    and simplification where the ranges of the predefined base types
    are required.

  - Simplifier version 2.04 ships on Windows and Solaris
    platforms with this release.  This includes improved proof
    tactics for enumerated inequalities, common SPARK idioms
    such as a "for" loop over an enumerated range, and simplification
    of quantified expressions.  The performance of the simplifier
    has also been greatly improved on large VCs.

  - Checker 1.47 ships on Windows and Solaris with this release. This
    includes extended rule families for dealing with modular arithmetic,
    bitwise operators and enumerated types.

This release re-inforces SPARK's position as the leading language
subset and static analysis technology for the construction of
high-integrity, critical software.

Please email us for more information at sparkinfo@praxis-cs.co.uk
or see www.sparkada.com

Yours,
  The SPARK Team
  Praxis Critical Systems

Note: The SPARK programming language is not sponsored
by or affiliated with SPARC International Inc and is
not based on SPARC(tm) architecture.