[GAP] Announcing the immediate availability of SPARK GPL 2010

[Jamie Ayre]

Dear GAP member,

We are pleased to announce the release of SPARK GPL 2010, the foremost
language, toolset and design discipline for the engineering of
high-assurance software. SPARK GPL is the version dedicated to the
academic and Free Software communities. This latest edition provides
many new features and enhancements in all areas of the technology.
The most notable ones are:

- A new tool named 'ZombieScope' which uses the SPARK proof technology
 to identify dead paths in SPARK source code.

- A new SPARK 2005 language switch, enabling an initial set of new 
 features for SPARK 2005. More features from Ada 2005 will be added
 to SPARK in future releases.

- Information flow policy checking, proving an automated means of
 checking that a SPARK program's information flow relations do not
 violate the specified safety or security policy.

- Function return annotations now appear as hypotheses in the VCs generated
 for subprograms that call those functions.

- A switch to enable checks for consistent casing in SPARK code and 
 annotations.

- The ability to generate cross-reference information files, enabling
 navigation features for SPARK code and annotations in GPS.

SPARK GPL 2010 comes with version 4.4.1 of the GNAT Programming Studio
IDE and GNATbench 2.4.0, the GNAT plug-in for Eclipse.

The SPARK GPL Edition is available on Windows, SPARC/Solaris,
Linux (both 32- and 64-bit) and Apple’s OS X (64-bit).

SPARK GPL 2010 can be downloaded from the "Download" section on
GNAT Tracker:

http://www.adacore.com/home/academia