Ada Resource Association

Stuart Matthews explains how SPARK 2014 uses and extends the features of Ada 2012 for automated verification of programs.

This two-part article discusses the benefits of developing code with automated static analysis, and then shows examples of doing so, using SPARK.

Static and dynamic code analysis can improve application performance, safety and reliability by identifying problems early in the development cycle if the proper tools and procedures are used from the start. Dr. Mike Hennell, founder of LDRA, spoke with me about the various aspects of these types of tools.

Zero Defect Software Development (ZDSD) is a results-oriented process that emphasizes the analysis, testing and reporting of the causality of defects. This process, which has evolved from the commitment to providing “five-nines” (99.999%) reliability for mission-critical applications, supplants the traditional approach of reacting to undesirable effects and treating symptoms while attempting to manage verification processes using “trend analyses” or simply tracking the occurrences of defects.

The ease with which code is analyzable depends of the language type you use. Static analysis is becoming mainstream, with mature bug-finding tools for C and Java, including products such as Coverity Prevent, Grammatech CodeSonar, and Fortify SCA. These products limit the level of “noise” (false warnings) inherent to such tools to a minimum. However, by carefully selecting those cases for which they report a problem, these bug-finders hide the fact that they are largely uncertain about the overall correctness of the program.

Static analysis tools are becoming more integrated into the software development process. Saving data from the compiler, change history, and error information during the process instead of as a post-code step can make static analysis more productive.

Jack Ganssle at Embedded.com discusses the Sofcheck and AdaCore CodePeer tool in Executing software contracts; in particular he examines the tool’s ability to create contracts for subprograms.