Slashdot Mirror
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?"
Reality is nothing but a collective hunch.
Seems like sensible future-proofing to me. Sure, the variable this is called this right now, but who knows what tomorrow will bring?
I'm scared of numbers that can't be written as a fraction. It's an irrational fear.
Exactly right. How can a program know what another program is *supposed* to do unless the first program has available to it an exact description of what the program it is checking is supposed to do? And if that exact description is available, there should be an automatic code generator which turns the description into code.
In other words, writting the exact description of what you want should be your last step in development, after which a code generator creates the program. This turns coding into the problem of writing the exact description. But can the exact description be analyzed? For contradictions and potentially missing parts I suppose, but it can never tell you if that is what you wanted.
This is perfectly illustrated by a Dilbert cartoon hanging in my cube in which Alice is trying to get program requirements from a user:
Alice: "I'll need to know your requirements before I start to design the software. First of all, what are you trying to accomplish?"
User: "I am trying to make you design my software"
Alica: "I mean what are you trying to accomplish with the software?"
User: "I won't know what I can accomplish until you tell me what the software can do"
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?"
Non-Linux Penguins ?
How could a program ever find this bug:
if (vote == "democrat")
{
republican++;
}