At the SPARK User Day yesterday in Bath, Altran-Praxis and AdaCore announced that the SPARK language will undergo a major transformation, to both extend the subset of Ada included in SPARK, and to use the new specification features of Ada 2012 instead of special comments like in today’s SPARK language. This is only fair that, SPARK annotations being the source of inspiration for many of the new specification features in Ada (pre- and postconditions, quantified expressions, etc.), their executable Ada version is now included in SPARK. This future version is expected to be released Q1 2014.
This is something we have been working on for almost 3 years now, between Altran-Praxis and AdaCore, inside the Hi-Lite project. We have been able to show that, not only we can extend the range of programs which can be proved automatically correct with respect to their specification, but we can combine much more easily testing and formal verification than what was considered possible until now.
Given the results achieved already, some (like the Microsoft researcher Rustan Leino who asked me this question at the SPARK User Day) could wonder why we don’t plan to release a product sooner. This was answered by a current SPARK customer, Robert Dorn from Secunet, who said that they want “first, that the future SPARK language and toolset allows them to express and prove as much as the existing one, and only then, that it extends the language and provides improved and new tools”. The work done in Hi-Lite is mostly concerned with automatic proof of functional properties. We are now working also on the expression and verification of data and information flow properties that are so important for many SPARK users.
We will continue to provide GPL releases of prototypes of these future tools to the community in 2013.