Tuesday, May 26, 2009
"A Direct Path to Dependable Software"
"A Direct Path to Dependable Software" is the title of a recent article in the CACM. It piques the interest, but otherwise has few details on how the approach would work. But an interesting quote:
As the required level of confidence rises, though, testing soon becomes prohibitively expensive, and the use of more sophisticated methods is likely to be more economical. Invariants may be harder to write than test cases, but a single invariant defines an infinite number of test cases, so a decision to write one (and use a tool that checks all the cases it defines) will pay off very soon.
posted by Berend de Boer @ 07:08 
Comments:
<< Home
Thank you for that, Berend. The same also applies to preconditions and postconditions: they define multiple test cases at once.
Naturally, the specifications are only the first step because they don't offer any assurance that the implementation complies.
With a good specification, you can (1) reason about the code effectively and efficiently, (2) test the code by exercising it, (3) test the code automatically e.g. with Autotest, and (4) apply mathematical proofs of correctness to those parts of the system which are amenable to it (ideally the compiler should be doing this).
Roger.
Post a Comment
Naturally, the specifications are only the first step because they don't offer any assurance that the implementation complies.
With a good specification, you can (1) reason about the code effectively and efficiently, (2) test the code by exercising it, (3) test the code automatically e.g. with Autotest, and (4) apply mathematical proofs of correctness to those parts of the system which are amenable to it (ideally the compiler should be doing this).
Roger.
<< Home
