SPARK GPL Edition
2010 Edition Now Available!
SPARK GPL provides the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines the renowned SPARK language and verification tools from Altran Praxis with the GNAT Programming Studio (GPS) and GNATBench development environments from AdaCore.
This release includes:
- 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.
The SPARK GPL Edition is available on Windows, Linux (both 32- and 64-bit) and Apple’s OS X (64-bit).
AdaCore and Praxis are dedicated to developing the finest tools available for software development with SPARK and Ada. The SPARK GPL Edition is the development environment for Free Software development and the GNAT Academic Program for use in Academia. SPARK Pro is for commercial/industrial development.
The SPARK GPL Edition consists of the following technologies:
- The SPARK Language Definition
- Full SPARK Toolset, including Examiner, Simplifier and Checker
- Supporting SPARK tools: SPARKSimp, SPARKMake, SPARKFormat and POGS
- Tutorial material for SPARK GPL and SPARK Pro are included in the accompanying release of the Tokeneer Discovery package.
