| SPARK Release 7.6
July 2008
Praxis High Integrity Systems is pleased to announce the immediate
availability of Release 7.6 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.6.
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.6.
Release 7.6 includes many significant improvements, including:
Corrections to the VC Generator for narrowing subtype conversions
involving enumerated types.
Record types that have a single field which is a predefined
scalar type are now allowed to be Atomic in RavenSPARK mode.
Improvement to the default-invariant generator where a
variable controlling a dynamic "for" loop is know
to be mode "in".
Simpler FDL modelling of the 'Pos and 'Val attributes of
type Character.
Better modelling of T'Valid for a subtype T in proof rules.
New "Output_Directory" option for the Examiner.
New "order" option for SPARKFormat that allows
for alphabetic or declaration-ordering of reformatted annotations.
Improved VC Generation for local variables in subprograms
that indirectly import an external own variable.
Improved performance in the Simplifier where user-defined
proof rules give rise to conditions that are fully instantiated.
New options on SPARKMake to suppress generation of the
index and/or meta-files and to process sources that don't
have a main subprogram.
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.
|
