[GAP] Announcing the availability of SPARK GPL 2011

[Jamie Ayre]

Dear GAP member,

We are pleased to announce the release of SPARK GPL 2011, 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:

- Automatic selection of flow analysis mode
The Examiner now supports automatic selection of information flow
or data flow analysis on a per subprogram basis. 

- Derived Numeric Types
Definition of numeric types has been made easier in GPL 2011 by the
introduction of language and tool support for explicitly derived
numeric types.

- SPARKBridge preview for Windows
SPARKBridge - a bridge between the SPARK tools and Satisfiable 
Modulo Theories (SMT) solvers - is now available as a preview to
Windows users, allowing them to trial alternate provers for 
discharging Verification Conditions.

- Library Additions
The SPARK library has been augmented with several new packages
including:
Interfaces
Ada.Characters.Handling
Ada.Text_IO

- Improvements to Proof Tools
The Simplifier now has enhanced reasoning capabilities for modular
types, allowing more proofs to be automatically discharged. In
addition, the proof summary output (from the POGS tool) has been
improved to make the management of the proof process easier for 
large projects.

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

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