ANNOUNCE: v5 SPARK tools now available

ANNOUNCE: v5 SPARK tools now available

[r_c_chapman]

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

This release is available free-of-charge
to academic institutions for teaching and non-commercial
research purposes.  Full support for this release will
be available to a single point-of-contact per
institution.

SPARK remains the only widely-used, unambigous programming
language that supports formal development methods such
as B and Z, while being used in large, real-world
projects such as EuroFighter, Lockheed C130J, SHOLIS,
and the MULTOS CA.

To accompany release 5, a second printing of the textbook
"High Integrity Ada - The SPARK Approach" by John Barnes
is in production.

Release 5 adds significant functionality over
previous releases, including:

Support for proof of programs involving abstract state;
Support for explicit quantifiers in predicates;
Improved generation of proof rules for enumerated types;
Generation of output files in HTML;
Command-line selectable annotation character;
Revised SPARK_IO package complying with the INFORMED design approach.

Please email us for more information at
 mailto:sparkinfo@praxis-cs.co.uk

or see our web-site:
 http://www.praxis-cs.co.uk/

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.



Sent via Deja.com http://www.deja.com/
Before you buy.