SPARK Pro is a product jointly developed by Altran Praxis and AdaCore that provides the language, toolset and design discipline for engineering high-assurance software. The developers say that the new version 11 of SPARK Pro offers many enhancements related to the way that functions and proof functions are handled. These changes are said to improve project efficiency by eliminating the vast majority of rules that previously were encoded manually. The main changes include a more powerful language for specifying proof functions and the ability to use the functions in any proof context. This greatly simplifies the task of writing and maintaining functional contracts for critical software, providing high assurance at lower cost. SPARK Pro combines Altran Praxis' SPARK language and verification tools with AdaCore's GNAT Programming Studio and GNATbench Integrated Development Environments. There are SPARK versions based on Ada 83, Ada 95 and Ada 2005, so all standard Ada compilers and tools work out of the box with SPARK, say the companies
