By Jack Ganssle

CodePeer

Summary: A new tool writes DBC-like contracts for you.

Almost a decade ago a number of static analyzers began to appear in the market. A number of such products exist now, including those from Coverity, PolySpace (now part of The MathWorks), Grammtech, Green Hills, Klocwork and others. (For an interesting discussion of what Coverity has learned in making the transition from academia to the commercial marketplace, see "A Few Billion Lines of Code Later" in this month's Communications of the ACM). Static analyzers examine your code to find runtime bugs. While quite expensive today, most of the developers I know who are using the tools agree that they are effective. Expensive, yes. Sometimes slow. And they hardly find all of the bugs. But they do find some of the tough ones.

C programs are, of course, particularly vulnerable to problems like memory leaks, so it seems the biggest market for these products is in that domain. But even safe - or at least safer - lingos like Ada are not immune to difficult-to-find bugs. Now AdaCore has teamed with SofCheck to bring the latter's static analyzer into the world of Ada systems. The resulting CodePeer product seems like a very worthwhile addition to an Ada programmer's toolbox.

But CodePeer is much more than that.

One of the oldest precepts in programming is to check your goesintas and goesoutas. A square root routine that's grounded in the real domain should toss an exception if one passes a negative number to it. But how many functions check their parameters?

Nearly a quarter century ago Betrand Meyer invented "Design by Contract" which codifies these checks (for more info see my articles here: http://www.embedded.com/columns/breakpoint/197008824?_requestid=265273). In DBC one defines formal contracts that check functions' inputs and outputs. Some languages, like Eiffel, provide built-in support for contracts. In C one uses work-arounds with a preprocessor or tortured assert() statements. Regardless, DBC is a philosophy of the developer manually writing out the contracts.

CodePeer twists this idea in an intriguing way. It examines the code and creates the contracts for you. They get embedded into comments and are not executable, but they provide clear cues to the developer that things may not be as they should. For instance, in this snippet from AdaCore's web site the postcondition (labeled "post") immediately makes it clear that the function has a glaring bug:

Just imagine how much more effective a code inspection would be given this information!

The tools does much more, but this is an indispensable aid to the Ada developer. Bugs are tough to find and potentially hugely expensive (think: Toyota).

For more on CodePeer see: http://www.adacore.com/home/products/codepeer/ .

Published January 27, 2010