Break Points
Executing software contracts
Jack Ganssle
2/15/2010 12:41 PM EST
(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 jack@ganssle.com. His website is www.ganssle.com.
Comments
krwada
2/16/2010 2:08 PM EST
If one were to put range checking and exception handling in every single function ... I would hazard a guess that this would add at least 15-20% overhead in code size. For deeply embedded systems ... this may not be so good. What I have found however, is if we place exception handling at critical points:
- Device drivers
- User input
- Network Management interfaces
.
... We can get a much better leveraging of exception handling and range checking within these areas. Also, there may be times that MACRO substitutions such as ASSERT() may be a decent alternative. It is better to let the bugs surface during testing than to surface out in the field.
Sign in to Reply
Larry Martin
2/18/2010 8:12 AM EST
krwada, I think your estimate of the overhead of intensive value checking is conservative. About 10 years ago, I worked with a Modula3 compiler for 80186 that provided such checks on each computation and array access. It easily doubled the size of the code. Think about it - in the source, you add two numbers together, thinking you are creating maybe 3 or 5 assembly statements, fetch-operate-store. In the assembly, though, the compiler adds checks to make sure unsigned variables have not gone through zero or done other inappropriate things. Those checks require their own fetches and operations, easily doubling the size of the assembly code. That particular compiler had a fun habit of resetting on any exception, making byte-level math a real minefield.
That said, I think Jack was writing about something else. It looks like this tool automatically generates unit tests and places comments that document the range of return values. That's pretty cool, IMO.
Sign in to Reply
ewm
2/20/2010 2:21 PM EST
The example smells a bit fishy.
I would expect DaysInMonth(7) to return 31.
Unfortunately, neither the code nor the #post contract appear to agree with me.
The code will return NumberOfDaysSince(Month=>7), which appears to count the number of calendar days elapsed since the given month.
The contract appears to say that the return value will be one of 0, 31, 59, ...
OK, so 31 is in there, so my hypothetical DaysInMonth(7) would meet its postcondition. But the other values in the postcondition make it clear that the writer expects the DaysInMonth function to return not the number of days in the specified month, but the number of days preceding that month on the calendar.
And even that doesn't appear to be specified correctly! The postcondition appears to expect the return value for March to be 59 (i.e. 31 days in January + 28 days in February), so leap year isn't handled by the postcondition.
It looks to me like the function is described three ways: (1) in the postcondition metadata, (2) in the code, and (3) in the "Oops! ..." comment. Of the three only the "Oops! ..." comment appears to be correct.
Sign in to Reply
on_the_road_to_tau
4/14/2010 5:17 PM EDT
Yes, ewm, month 7 should return '31'...that's the bug...and you can see that because of the post-condition that CodePeer has inserted, which details the values that the function can return (and only those values).
Sign in to Reply