Executing software contracts
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), Grammatech, 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 column on "Contracts put the 'I do' in code" ).
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 the snippet below 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 tool does much more, but this is an indispensable aid to the Ada developer. Bugs are tough to find and potentially hugely expensive (think: Toyota).
(Editor's Note: Jack's Embedded Poll Question this week is "Do you use executable contracts?" To vote go to the Embedded.com Home Page)
Jack G. Ganssle is a lecturer and consultant on embedded development issues. He conducts seminars on embedded systems and helps companies with their embedded challenges. Contact him at firstname.lastname@example.org. His website is www.ganssle.com.