ANN: SPARK Release 7.2

ANN: SPARK Release 7.2

[Rod Chapman]

We're pleased to announce the immediate availability of
Release 7.2 of the SPARK Language and Toolset.

This release incorporates several significant improvements.  Full
details are available in the Release Note, which is available
from www.sparkada.com.

For readers of the SPARK Textbook, upgrade packages are also
available from www.sparkada.com including the new language definition,
manuals and demonstration tools for IA32/Windows and IA32/Linux.
These upgrade packages are also available from the "SPARK Book"
page of www.sparkada.com as usual.

Supported professional customers are being sent upgrades now.
Academic users and tool-partners will receive their upgrades shortly.

Some technical highlights of this release include:

Language:
Full-range record subtypes are now supported.

Rules for passing array elements as "in out" parameters have been
relaxed
(this significantly eases the construction of iterator algorithms.)

String constants that are constrained by their initializing
expression
are allowed.

Finally, instantiation and use of Unchecked_Conversion is permitted.

Examiner:
Flow analyser more accurately models "for" loops that have a static
range.

New VC Generator model of "for" loops correctly models all loops,
including those with a dynamic range where variables controlling the
loop exit are modified in the loop body.

Declaration of subprograms in the private part of a package is
implemented.

VC Generator produces hypotheses showing that local variables are
"in"
their designated subtype.

A new "brief" error message mode eases integration with EMACS and
GPS by
producing "gcc style" errors that can be recognized by such
environments.

Information flow errors are produced by default in a new
easier-to-read
format.

Refinement proofs between the private and full view of a private
type
are now supported.

The VC Generator can now produce replacement rules for composite
constants,
under the control of a new command-line switch and a new annotation.

Simplifier:
New tactics for quantified expressions, structured object updates
and
scalar inequalities.  These give a significant improvement in
Simplifier "hit rate" (aka Completeness) for common SPARK idioms,
and particularly for proofs of exception freedom.

SPARKSimp supports multi-processor machines for improved throughout
(NOT available with the Demo toolset...)

Other:
A new utility "SPARKMake" that automates the production of Examiner
index files and meta-files.

Yours,
 Rod Chapman, SPARK Team.