SPARK Release 7.5

May 2007

Praxis High Integrity Systems is pleased to announce the immediate availability of Release 7.5 of the SPARK language and the SPARK toolset.

Full details of all language and tool changes can be found in the release notes for release 7.5.

Supported, professional customers will receive upgrade packages immediately.

Buyers of the "SPARK Book" by John Barnes can now download upgrade packages to bring their toolset and documentation up to release 7.5.

Release 7.5 includes many significant improvements, including:

Corrections to the VC Generator for exported parameters where the actual parameter is an array element or a record field, and for explicit modular subtype conversions.

Additional warning control file keywords for default loop assertion and real RTC warnings.

Reduced memory usage in the Examiner.

VC Generation for values of type Ada.Real_Time.Time when in RavenSPARK mode.

Improved static semantic checking of the arguments of pragmas.

The Simplifier now reports all uses of user-defined proof rules in the Simplifier Log (SLG) file.

POGS now collates and reports all uses of user-defined proof rules in its summary output.

New "Summary only" option in POGS.

Improved Simplifier tactics for proof of scalar inequalities where transitivity is involved.

Please email us for more information at sparkinfo@praxis-his.com

Yours,
The SPARK Team
Praxis High Integrity Systems

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