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

a chain of crutches

[fred fleenblat]

I dunno, as more tools to verify code become available, businesses will hire cheaper and sloppier programmers and just force all the code through the verifiers and hope for the best.

These aren't tools to make the best code better, they are tools to make the worst code okay.

Not possible

[Intron]

The problem with any verification tool is that it can't know what you expect the program to do unless you tell it. Why should this be any more correct than the program itself? In other words, if you can write a description of what the program should do that is more accurate than the program, then that description should replace the source code.

Re:No :)

[Control Group]

The steps in his methodology are counter-intuitive and therefore stupid

I agree with your general statement, but this isn't good evidence. Plenty of things are counterintuitive, yet correct and useful.

I present exhibit A: the whole of statistics. It is counterintuitive that after the tenth straight "heads" result, the eleventh flip still has even odds of coming up heads - despite the fact that the odds of eleven straight flips coming up heads are 2048:1. It is counterintuitive that you should always switch doors in the Monty Hall problem.

Or, if you're scientifically minded, I give you relativity. It is counterintuitive that no matter how fast you're moving relative to a light source, the speed of the light from your point of view will never change.

It is counterintuitive that gravity causes hot air balloons to rise, or that the way to escape Earth orbit is to accelerate along it, not away from Earth.

Counterintuitive doesn't necessarily mean that something's incorrect.

Re:Yes, it works, but it's not easy

[Animats]

What is the semantic difference between C and Pascal?

The big problems with C/C++ from a formal methods standpoint:

• void* (You lose all the type information)
• Too much casting. (Again, you lose all the type information)
• Array size information isn't carried along with arrays or passed through function calls. (Biggest design mistake in C).
• The "array is a pointer to the first element" convention. (Is this an array or a single object?)
• Pointer arithmetic semantics are ill defined. (Long story.)
• C++ iterators don't have an explicit tie to the collection, so detecting iterator invalidation statically is hard.
• Hard to detect aliasing. (A consequence of the free use of pointers.)
• Too much "undefined behavior" that isn't prohibited.

I would expect pointer arithmetic to be the source of problems, but if I recall correctly, Pascal's pointers have arithmetic as well.

No, they don't.

Pointer arithmetic really is obsolete. Compilers have been generating code for subscripting that's as good or better than pointer arithmetic code for well over a decade now.