原创 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.

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. 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 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.

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).