15 ms·
It means that a program has been verified against a model, and properties of that model are held true. What it does not mean is that the program is bug free. T
by staticassertion 4y ago
It means that a program has been verified against a model, and properties of that model are held true.
What it does not mean is that the program is bug free. That would, of course, violate the halting problem, or its generalization Rice's Theorem - non-trivial programs can not have arbitrary properties proven about them.
There's also Gödel's Incompleteness Theorem, obviously, as well as the fact that a proof is only as good as its model.
- UncleMeat 4y agoIt wouldn’t break Rice’s Thm to prove it for a particular program. All Rice’s Thm says is that any algorithm must fail on some programs.
- staticassertion 4y agoIt would if you're talking about arbitrary classes of bugs.
- UncleMeat 4y agoNot so. Consider the algorithm that reports "Yes" for all inputs for all program properties. For a large number of programs and properties, this algorithm will report the correct information.
- mbrodersen 4y agoNot true for non-Turing complete languages. Which is why all proof tools require a proof of termination. Some do it automatically (essential ruling out Turing complete languages) others require a formal proof of termination by the user.