CodePeer generates the contract for a procedure when none exists allowing a developer to see what the procedure will actually do with inputs and outputs Click here for expanded view Image courtesy of Adacore

Best of 2015: CodePeer SPARKS Ada

Dec. 4, 2015

Adacore’s CodePeer takes verification of Ada code to the next level.

Some tools need time before they become refined and really useful. That was the case with Gumstix’s Geppetto (see “Create Custom Capes Fast and Easy” on Electronic Design). Geppetto recently added support for processors and popular platforms like Raspberry Pi to the PCB design and delivery system.

This is also the case for Adacore’s CodePeer. CodePeer analyzes Ada programs looking for run-time and logic errors. It is similar to many static analysis programs designed to identify errors in C, C++, and Java applications, but CodePeer has an advantage. Ada tends to be more rigorous with programmers with the advantage of allowing developers more precise control over the application. The Ada 2012 standard goes farther by providing support for contracts (see “Ada 2012: The Joy of Contracts” on Electronic Design).

A more restricted subset of Ada 2012 is SPARK. It allows formal methods to be used in proving a program will meet the specified requirements that are specified using Ada contracts. Some sample output from CodePeer (see the figure) highlights how this works.

Ada 2012 contracts allow definitions for procedure, modules, and other code entities to include pre-conditions and post-conditions like those shown in the example. In this case, the argument N must be a positive Natural number. A zero of negative value would generate a runtime error.

Electronicdesign Com Sites Electronicdesign com Files Uploads 2015 06 Capture Format

CodePeer can generate the contract information and will compare it with any contracts that programmer provides as well. The CodePeer contract could also be moved into the code as well, making the code more robust since changing the code without changing the contract would allow the system to detect an error where the new code now conflicts with the promised contract.

Of course, CodePeer also detects conflicts between its actual contract and any the programmer provides. It also flags errors so that even a banker could not write a contract that would work.

Any static analysis program including CodePeer can generate false positives. It tends to do better than other tools because of the language being analyzed. Languages like C allow programmers to easily shoot themselves in the proverbial foot and they typically do so, much to the chagrin of users of the programs.

There are many myths about Ada and it does not command the interest that C or C++ does in the embedded realm, but the rise of the Internet of Things (IoT) —along with its security and reliability issues—should bring Ada into a better light. Ada and CodePeer can have a major impact in the quality of any code for IoT or other applications. Ada has moved past its military and aviation roots to other transportation arenas, including trains and automotive.

About the Author

William G. Wong | Senior Content Director - Electronic Design and Microwaves & RF

I am Editor of Electronic Design focusing on embedded, software, and systems. As Senior Content Director, I also manage Microwaves & RF and I work with a great team of editors to provide engineers, programmers, developers and technical managers with interesting and useful articles and videos on a regular basis. Check out our free newsletters to see the latest content.

You can send press releases for new products for possible coverage on the website. I am also interested in receiving contributed articles for publishing on our website. Use our template and send to me along with a signed release form.

Check out my blog, AltEmbedded on Electronic Design, as well as his latest articles on this site that are listed below.

You can visit my social media via these links:

I earned a Bachelor of Electrical Engineering at the Georgia Institute of Technology and a Masters in Computer Science from Rutgers University. I still do a bit of programming using everything from C and C++ to Rust and Ada/SPARK. I do a bit of PHP programming for Drupal websites. I have posted a few Drupal modules.

I still get a hand on software and electronic hardware. Some of this can be found on our Kit Close-Up video series. You can also see me on many of our TechXchange Talk videos. I am interested in a range of projects from robotics to artificial intelligence.