ANN: SPARK Toolset Release 6.0 now available

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

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

Commercial supported customers will receive their
upgrades within the next few days.  Tool partners
and academic users will be upgraded following that.

A new edition of the "SPARK Book" by John Barnes
is also planned.

Release 6.0 adds significant functionality over
previous releases, including:

 Support for "external variables" - these allow the
automated modelling of volatile input and output "streams"
to and from a SPARK program.  Our "INFORMED" design approach
has been updated to illustrate the use of external variables.

 Modular types with binary modulus are supported in SPARK95 mode.
Bit-wise logical operators are permitted for such types.

 A new "derives null from ..." annotation form allows the
declaration of procedures which take parameters, but
have no observable effect on any state within the 
SPARK boundary of a program.  This is particularly
useful in the construction of data-logging packages,
testpoints, diagnostic code and so on.

 VC-Generation in much improved.  In particular,
fewer hypotheses are generated for most VCs, resulting in 
faster simplification of those VCs.

 SPADE Simplifier version 2.00 ships on Windows and Solaris
platforms with this release.  This includes improved proof
tactics for modular expressions, bit-wise logical operators,
and inequalities involving enumerated types.  The new Simplifier
behaves identically on Windows and Solaris.

 A new tool called "SPARKSimp" is supplied on Windows and Solaris.
This is a "make" style tool for the Simplifier which assists
in the proof of large programs.

This release re-inforces SPARK's position as the leading language
subset and static analysis technology for the construction of
high-integrity 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.