Don wrote: > You can certainly catch bugs with that technique, but the word "proof" > has no business being there. It's like the "unsinkable" Titanic. > (I think it's really similar, actually. Apparently the only reason the > Titanic sank was that many of the rivets were defective).
Actually, the word "proof" is perfectly appropriate. You just have
to remember that *any* proof relies on some starting hypothesis.
What a theorem prover does is, given a certain set of starting
conditions, and a certain set of assertions to check, they will tell
you:
- Either that the assertions will fail, in which case they will
provide an example of valid starting conditions and an execution
path that causes the failure;
- Or tell you that the assertion will always pass. In which case,
barring bugs in the theorem prover, you can be 100% sure that so
long as the starting hypothesis hold then the assertion will pass
(compiler and hardware reliability are always part of the starting
hypothesis);
- Or that they cannot conclude.
What I just said refers to the *theorem* prover itself. A
*software* prover (like Klocwork) contains some extra code to
extract some starting hypothesis and some assertions from your
source and give them to the theorem prover, then post-process the
results to make them usable. This has several important implications:
- Usually, the software prover will not make the distinction between
options 2 and 3: if an assertion cannot be proven to fail, then it
will be silently assumed to pass;
- Everything depends on the assertions that the software prover
uses. Some of them are easy to define (when you dereference a
pointer then that pointer must be valid, or if the source code
contains a call to "assert" then that "assert" must pass), but some
are a lot less obvious (how do you define that "the output must make
sense"?)
> My recollection from university courses was not that "proofs will find
> bugs in your programs". Rather, it was that "proofs will ensure your
> program is correct".
>
Well, I haven't taken any formal university courses on software
provers, but if that's the approach your teachers took, then they
were wrong (unfortunately, this is a kind of mistakes teachers are
very often prone to).
Jerome
--
mailto:jeber...@free.fr
http://jeberger.free.fr
Jabber: jeber...@jabber.fr
signature.asc
Description: OpenPGP digital signature
