Why don't other programming languages have ranges?

["Jérôme M. Berger"]

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:jeberger at free.fr
http://jeberger.free.fr
Jabber: jeberger at jabber.fr

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <http://lists.puremagic.com/pipermail/digitalmars-d/attachments/20100730/9e52383a/attachment-0001.pgp>