[GAP] Announcing the immediate availability of GNAT GPL and SPARK Hi-Lite GPL

[Jamie Ayre]

Dear GAP member,
 
We are pleased to announce the availability of GNAT GPL 2013 and SPARK
Hi-Lite GPL. GNAT GPL 2013 provides new Ada 2012 language features,
introduces new tools and new versions of existing tools, incorporates
a range of improvements and adds several new platforms. Some of the
key enhancements:
 
New Language Features
- Final touches on Ada 2012 support
- Automatic Endianness conversion (‘Scalar_Storage_Order)
- Dimensionality checking (new aspects and packages)
 
New version of existing tools
- GtkAda
Gtk+ version 3 brings new widgets, a CSS-based theming framework,
and an improved API that has been clarified and has a more
homogeneous naming scheme.
- New versions of IDEs
- GPRbuild
- GDB debugger
 
Switch to GCC 4.7 back-end
 
New GNATcheck rules
 
SPARK Hi-Lite GPL 2013 is a package that can be installed after
GNAT GPL 2013, to provide access to the new SPARK toolset being
developed in project Hi-Lite. This release is a major evolution of the
SPARK toolset providing formal verification for a subset of Ada
programs.  This new toolset uses Ada 2012-style contracts (e.g.
pre- and postconditions), instead of the stylized comments in
previous versions, to provide specifications of programs. The benefits
of this new version are:
 
- larger supported subset of Ada (including generics, discriminants, etc.)
- same contracts used for testing and formal verification
- applicable to units partly in SPARK
- improved automatic proof of complex contracts
- new integration in GPS
 
A preview of the data and information analysis is also available. For
more information on SPARK 2014, please visit www.spark-2014.com.
 
Both toolsets can be downloaded from the "Download" section on
GNAT Tracker:
 
http://www.adacore.com/academia