Is Code Verification Finally Good Enough?

Jonathan asks: "As someone who has been following the development of software verification technology, a recent trend has intrigued me. It seems that the formal method people have finally come down off their high horse and are offering code verification as just another tool. This approach shows up in recent Java and C# based code verification tools that aren't aimed at 'proving correctness' so much as finding potential errors. Now it seems that such an approach is beginning to find its way into XP methods[pdf] as another verification tool to supplement unit tests. Given the current speed and effectiveness of tools like the Spec# verifier, is code verification via automated theorem proving finally going to make its way into the mainstream?"

Comments

Re:a chain of crutches

[chroot_james]

they already do! I came across this the other day:

private getThis() { return this; }

Re:a chain of crutches

[kirun]

Seems like sensible future-proofing to me. Sure, the variable this is called this right now, but who knows what tomorrow will bring?

To quote Knuth

[dargaud]

"Beware of bugs in the above code; I have only proved it correct, not tried it." —Donald E. Knuth.

Re:Not possible

[l33td00d42]

Alice: "Try to get this concept through your thick skull: the software can do whatever I design it to do"
(pause)
user: "Can you design it to tell you my requirements?"

boy, that's easy:

print "This software is required to print this statement.";

logic bug

[hey]

How could a program ever find this bug:

if (vote == "democrat")
{
        republican++;
}