Kay Schluehr <[EMAIL PROTECTED]> writes: > Sure. But knowing that memory is limited doesn't buy you much because > you achieve an existential proof at best: you can show that the > program must run out of memory but you have to run the program to know > where this happens for arbitrary input values. Moreover you get always > different values for different memory limits. So in the general case > you can't improve over just letting the program run and notice what > happens.
Program verification is nothing like the halting problem. It's not done by dropping the program into some tool and getting back a proof of correctness or incorrectness. The proof is developed, by the programmer, at the same time the program is developed. Verifiability means that the programmer-supplied proof is precise enough to be checked by the computer. Think of when you first learned to program. Most non-programmers have an idea of what it means to follow a set of steps precisely. For example they could tell you an algorithm for sorting a shelf full of books alphabetically by author. Programming means expressing such steps in much finer detail than humans usually require, to the point where a machine can execute it; it takes a lot of patience and knowledge of special techniques, more than non-programmers know how to do, but we programmers are used to it and even enjoy it. Now think of something like a code review. There is a line of code in your program (maybe even an assert statement), that depends on some variable "x" being greater than 3. You must have had a reason for thinking x>3 there, so if the reviewer asks why you thought that, you can explain your argument until the reviewer is convinced. Do you see where this is going? Code verification means expressing such an argument in much finer detail than humans usually require, to the point where a machine can be convinced by it; it takes a lot of patience and knowledge of special techniques, more than most of us regular "practical" programmers currently know how to do, but the methods are getting more accessible and are regularly used in high-assurance software. In any case there is nothing magic about it--just like programming, it's a means of expressing precisely to a machine what you already know informally how to express to a human. -- http://mail.python.org/mailman/listinfo/python-list