Is Code Verification Finally Good Enough? 87
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?"
For what? (Score:3, Interesting)
It makes a difference which "good enough" you're asking for.
(The answers to those questions, to channel one Urban Chronotis, are yes, no, and maybe. Not necessarily in that order)
Re: (Score:2)
What should be verified (Score:2)
For Guaranteeing Correct Requirements? (Score:2)
Uh... no.
But they can probably be considered to be a newer and better version of lint, and that's a good thing.
Re: (Score:2)
Code-checking is a good thing, and provably correct code is especially good, though what's provable is still narrower than the range of behaviors of any interesting system I've seen.
But the most difficult part of any complex system development project is getting valid requirements and then implementing a process of systematically and iteratively confirming that the delivered system is what the users need, not what some bunch of managers or analysts asked for on their behalf. This is
Slowly work their way into the mainstream (Score:1)
Developers will have to analyze the specific tools and decide if it is a good supplement to current verification efforts or if it can replace some steps. I think though once it worms its way into mainstream (if only light) use, the tools will continue to improve and give us more options, and become a more integral part of verification.
I know from work I've done, th
"No" (Score:1)
Mankind's ability to write software is far in advance of mankind's ability to figure out what it does or does not do.
If Microsoft ship 100 million copies of Windows Vista to 100 million people on public Internet, where the people have mutually-incompatible agendas, then at least some of the people will end up unhappy.
a chain of crutches (Score:2, Insightful)
These aren't tools to make the best code better, they are tools to make the worst code okay.
Re:a chain of crutches (Score:4, Funny)
Re: (Score:3, Funny)
Re: (Score:2)
It got funnier the more times I read it. The first time, I read it as a private accessor function that returned a private class member. That alone would be funny, since the only reason to make such a function would be to allow read-only exposure of a private member to non-class code, and by making it private, that eliminated the usefulness altogether. Then, I realized precisely which member was being returned. When I realized that it wasn't returning an explicit class member, but rather, a pointer to th
Re: (Score:2)
Or perhaps the .getThis() method was specificed by an interface as a way of retrieving some functionality, but the functionality was implemented by the class itself. This design is used in table cell renderers in Java for example.
Re: (Score:2)
Or at least, if they did, its in a language that just happens to look like Java, but where "this" isn't a reference to the object the object the private method is in. Because that makes my brain hurt.
Re: (Score:2)
I've never seen anything quite that bad, but I do see this a lot in older code:
The explanation for that is often that someone will create a function to go fetch a single piece of data, getHeight(). Then the next programmer comes along, and adds the ability to getWidth(). The next guy starts to add getDepth(), but then thinks that this is a bad path to go down, so writes a new function called get_value() that serves the more general purpose of fetching data
Re: (Score:2)
This brings up a somewhat interesting point. I can see the point of using stuff like getFoo() just to access an attribute foo. I think it has its purpose (read-only access), but I can also see that it is rather ugly. Further, in C++ code you sometimes see the use of friend just to provide full access to certain attributes and methods otherwise kept hidden or read-only (through getFoo()) to certain privileged classes and such.
I think sometimes it might be more useful to provide proper access control f
Re: (Score:2)
Re:a chain of crutches (Score:4, Informative)
So to that end, model checkers (and other forms of checking) are Good Things(TM). The possibility that some will misconstrue checking facilities as a substitute for competent and disciplined engineers is a separate issue, and it's not the fault of the checking scheme. The *organizational* problem of poor recruiting cannot be solved by getting rid of model-checking systems, and if your recruiters think that talent can be replaced by a "verification" system, you've got bigger problems than merely the shoddy designs that will come down the pike.
(Please note that I prefer to use the term "check" rather than "verify", because the latter term, when used to describe a program, too easily connotes the notion that a "verified" program is free of any bugs (which is, needless to say, always a dubious claim). "Check" on the other had usually connotes the idea that there is a specific bug (or set of specific bugs) that is tested for. Of course, TFA mentions they don't want to imply that (verification == no bugs). But IMHO too many people make that mistake.)
Re: (Score:1)
Everyone 'wants' to use tools but the reality is the overhead is pretty significant so they are avoided. Only in large companies do I see this methodology and even that is f
No (Score:1)
Not possible (Score:2, Insightful)
Re: (Score:2)
Your example 2 - of course it's easy to check if the result is sorted. That's called QA, not verification. Verification would be proving that the quicksort routine sorts the array for all possible inputs. Proving that it implements quicksort and not a sort that has slightly worse performance is an even harder problem.
So no, you did not dispr
Re: (Score:2)
You see, you totally missed the point of my comment. (A) "The compiler could do it" is the same as saying the compiler is a veri
Re: (Score:2)
There are many simple things that a program verifier can check for. I can see a program figuring out that your foo(NULL) call is always going to be wrong (e.g. by having the verifier notice that you are dereferencing it without checking if it is NULL and adding an assertion to the exported definition of the function; in this case the assertion will be a constant so it can be a compile-time error).
A lot of the "variable may be uninitialized" errors that a good compiler will spit out are along those lines.
Re: (Score:2)
This is a good example of why code verification is a hard problem. You may be able to tell from the given code fragment that c is always initialized, but I can't. Specifically, when "float n = 0.5;" it seems to me pretty clear that c isn't initiali
Re: (Score:2)
You make a good point, but since I was only giving code fragments, you didn't see that this was C code and n was declared as an int parameter...but, let's say it's a dynamically-typed language, should it flag this code fragment as the error, or the location where I call it with a value that it can't prove is = 1? You can go a long way with assertions, and a program verifier can use assertions to guide it in it's proofs (although the assertions have to verifiable from the code, which means you have to lay o
Re: (Score:1)
Then c and b will both be uninitialized.
You can't trust initialization in conditional statements unless you cover all conditions or if you declare your variables within the conditional code block.
Re: (Score:2)
b and c will be uninitialized outside the loop, true, but they aren't used outside the loop. Note that I don't declare the variables, inside or outside the loop, and it isn't even necessarily C code. Even if b or c are used later, it could well be that they are used in a context where n is known to be >= 1. You can't read more into code fragments than what is presented.
If I were to use b or c after the end of the loop (with no other initializations or conditions), then a program verifier might add in
Re: (Score:1)
Then your arguement would hold water, but as it is hope for the best, but plan for the wors
Re: (Score:2)
I don't need a defense, I was giving an example of code that current compilers don't analyze as completely as possible, as an example of the type of thing that a code verifier would have to be able to analyze in order to find obscure problems. It wasn't being held up as an example of fine programming.
I don't need to assume anything about b and c outside the loop, as I didn't give any code outside the loop. You're the one assuming for some reason that b and/or c would be needed after the loop. I was sayi
Re: (Score:1, Funny)
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 pr
Re: (Score:2, Funny)
Re:Not possible (Score:4, Interesting)
That way, you'll know when the two disagree. It doesn't prove that it does what you *intend* to do, but it proves that spec and source say the same thing. If they're written by different people, you can now have a fairly high degree of confidence.
Does it make your program bug-free? Only if you can write a bug-free spec. But it's a useful concept to reduce the likelihood of problems.
Use a language with build in prooving. (Score:1)
type Day_Of_Month is range 1
Neither Java nor C# allow that kind of controll over integer types. Mind you there is A# (Ada for CLI).
Martin
Re: (Score:1)
Well, they don't quite allow this control on integer types. But you don't need to use integer types, you can use an enum in Java (with methods for operations), and I _th
Re: (Score:1)
Once you know the month inside a Date class you can do more checks. But you won't need to check for the date to be >0 or 32 any more - theese cases have allready been handled.
Martin
Re:Not possible (Score:4, Informative)
It is often easier to describe what a program has to do than it is to describe exactly how to do it. I can describe what a square root finding algorithm has to do: given x it has to find y such that y*y =x; without coming close to writing something that actaully finds the square root. All the prover then has to do is ensure that the code instructions really do produce a result that satisfies the stated constraint - which is potentially entirely possible. Writing contracts for code can be as easy (or easier) than writing unit tests for code. If you write a contract instead of a unit test then that potentially gives the prover all it needs to verify that the code will work for all possible test cases instead of your predefined unit test cases. If the prover can't manage that then just feed in some test data and if the contract fails you've found an error (that is, at worst you've got a unit test already). Working this way can be remarkably efficient at weeding out errors - you verify code when it works, and essentially do unit testing for the code that can't be verified. Perhaps if you actually tried it you'd see.
Re: (Score:2)
I agree that it would be nice to see some simpler, cleaner languages, but I'm not sure if that's going to happen any time soon. For example... suppose the people who design model checkers for SML only have to do only X man-years of work, while the people who do model checkers for C# have to do 100X. So what-- the model checkers for C# are still going to be cheap and widely available, because there is a market f
Re: (Score:2)
Many aspects of the program can be described, and not all of them must be proven.
A program can be roughly divided to its requirements specification and the implementation. The requirements leave a lot of "freedom" to the implementation, and the choices in this area are not important to prove.
As a simple example, a "sort" algorithm has
Excuse me, did any of you graduate yet? (Score:1, Interesting)
Re:Excuse me, did any of you graduate yet? (Score:4, Informative)
You see, you should have learned before you graduated that just because a problem is hard (or impossible) in general, that doesn't mean the average case is hard at all.
Re: (Score:2)
Since when did this move from the realm of undecidable problems into solvable with a Turing Machine?
About as long as we've being using finite state machines as approximations to a Turing Machine.
No :) (Score:1, Troll)
The paper you linked to -- I just finished reading it. The "methodology" they provide has more comedic value than anything else. The steps in his methodology are counter-intuitive and therefore stupid. He wants us to iterate over each requirement, re-writing a function as the most simple program which passes the tests? What possible reason fo
Re: (Score:2)
I *REALLY* think you miss-interpreted the problem. The author clearly states the task is to build a function which gives all prime numbers smaller than n. Furthermore, what you've described is unit testing, which sadly is not a new concept.
Re: (Score:2)
Not every methodology sucks all the time. A methodology is just a named collection of practices.
Humans inherently crave religion. Convince someone that something works and they're likely to cling to it to the bitter end, be it Code Verification, atheism, voting Republican or whatever.
Re:No :) (Score:5, Insightful)
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: (Score:2)
"The way to write software is to design it, not have a random number generator spit out text, wait until a given chunk compiles, then test it to see if it does what you want."
And you say "that's not true, it will eventually produce a correct program! It might be easier to write a program by designing it, but that's a different question."
Anyway, if you are in orbit and you continually accelerate directly away from Earth (which means that you are continually changing your thrust vector as you continue to or
Re: (Score:2)
A lot of good code has been written using genetic programming and genetic algorithms, so I find it to be an erroneous or at least over-broad claim.
Re: (Score:2)
That's buoyancy.
Yes, it works, but it's not easy (Score:5, Interesting)
The main reason program verification didn't catch on was that it was hopeless for C and C++. The semantics of those languages were so messy that formalizing them was nearly hopeless.
Java and C#, however, are good enough. (So were Pascal, Modula, and Ada.)
Here's the manual for the Pascal-F verifier [animats.com], a system written by a team I headed back in the early 1980s. This was a proprietary system done internally for Ford Motor Company. Take a look at the example real time engine control program beginning on page 155. It was painfully slow back then; it took 45 minutes of VAX 11/780 time (1 MIPS) to verify that program from a cold start. Today, it would take about a second.
What's being proved in that example? First, that there are no subscripts out of range or arithmetic overflows. Second, that all loops terminate. (Yes, you can prove that for most useful programs; the halting problem applies only to pathological programs.) Third, that the following constraints hold:
Useful stuff, the conditions needed to keep the engine running.
This is "design by contract" with teeth. Each function is checked to insure that it always satisfies its exit conditions if its entry conditions are satisfied by the caller, and that the function doesn't overflow, subscript out of range, or fail to terminate. Each call is checked to insure that its entry conditions are always satisfied. The end result is a guarantee that those properties hold for the whole program.
This is a very valuable check. It insures that caller and callee are in agreement on how to call each function. That's the cause of a huge number of software bugs - the caller made some incorrect assumption about the function being called, or the function didn't check for something which it needed to check. Both of those can be statically machine checked.
It's not easy to get a program through formal verification with a verifier like that one. The verifier does almost all the work on easy sections of code, but where correctness depends on anything non-trivial, you have to work with the theorem prover to get the proofs through. This isn't easy. The DEC Java checker and Microsoft's Spec# checker aren't as hard-line.
Re: (So were Pascal, Modula, and Ada.) (Score:1)
And Ada isn't dead, it just got another rejuvenation in the form of Ada 2005: http://www.adaic.com/standards/ada05.html [adaic.com].
So the use of past tense was not appropiate.
Martin
Re: (Score:2)
Re: (Score:1)
I work for one of the named companies
Re: (Score:2)
What is the semantic difference between C and Pascal?
As far as I can remember, the only real semantic difference was Pascal's lack of casting.
Is this difference really the breaking point of C's provability?
I would expect pointer arithmetic to be the source of problems, but if I recall correctly, Pascal's pointers have arithmetic as well.
Re:Yes, it works, but it's not easy (Score:4, Insightful)
What is the semantic difference between C and Pascal?
The big problems with C/C++ from a formal methods standpoint:
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.
Re: (Score:2)
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.
That depends entirely on what you mean by "pascal". The pascal language as spec'd doesn't. But nobody uses that, so this not a very useful definition to adhere to.
Most users of "pascal" use/used Borland Turbo Pascal or Delphi. In those languages you *can* do pointer arithmetic. Sure you have to jump through more hoops and casts than with C (it can be considered
Re: (Score:1)
I tried hard, realy hard to get splints bound checking to work - but in the end it did not work out.
The project is not stalled since 2004 [2] and for me it is now clear that the "Secure Programming Lint" was a hopeless endeavor.
As for casting: Ada has about 3 different ways of type convertions and is still provable.
Re: (Score:2)
I have programmed in Assembly, Python, C, C++, Pascal, some Lisp and a tiny bit of Java, Haskell and Ada.
I dislike Ada because I believe there are far too many primitives that should be libraries (semaphores and other concurrency features).
I now love the other edge of the spectrum: Python. The "eww whitespace" barrier seems to block/filter a lot of closed-minded programmers, but don't let it prevent you from learning
Semaphores in Ada (Score:1)
There are some attempts of Rendezvous based threading for other languages but it proves difficult since you need some inter-task parameter passing mechanism. Remember that a Rendezvous is a bit like a function/procedure call only the parameters are passed from one task to another.
And parameter passing is a language feature and quite difficult to implement as a library. I know because I tried using by using Obser
To quote Knuth (Score:3, Funny)
logic bug (Score:3, Funny)
if (vote == "democrat")
{
republican++;
}
Re: (Score:2)
(haha)
Re: (Score:2)
Verification gets a boost from managed langs (Score:3, Interesting)
Please verify: (Score:2)
Please verify that
(define (foo n)
(cond
((= n 1) 1)
((even? n) (foo (/ n 2)))
(else (foo (+ (* n 3) 1)))))
returns 1 for any positive integer n.
Well typed-ness matters, not the halting problem. (Score:2)
Re: (Score:2)
For preventing buffer overflows, you will have to prove that some value being used as an array index is an integer in the range from 0 to the size of the buffer minus 1. In this case, the problem is to prove that the result is an integer in the range 1 to 1. Most type systems aren't exp
Re: (Score:2)
Generally, proofs for this are expressed as loop invariants inside of functions, and as predicates on the entry and exits of functions. If a function takes an array index as a parameter, there is a predicate that 0<=i<n, and it is the responsibi
Re: (Score:2)
Otherwise, it doesn't.
Can your type system prove that there is no buffer overflow?
Coming from the hardware side... (Score:1)
I have often wondered why more formal techniques aren't deployed in the software world.
As has been mentioned here, the thing about formal is that you will often "stump it" and so you may need to "help it" in complex, real world desi
Re:why more formal techniques aren't deployed (Score:1)